PV4 ⊧ DepthKchecks safety properties for a C program

DepthK is a software verification tool that employs a proof by induction algorithm that combines k-induction with invariant inference

Application domain/field

• Software verification
• Bounded model checking
• Model checking

Type of tool

Model checker

Expected input

• C program
• Safety property

Format:

• C program: .i file
• Safety property: .prp file

Expected output

TRUE and a witness if there is no path that violates the safety property, FALSE and a witness if there exists a path that violates the safety property or UNKNOWN otherwise. The witness is stored as a .graphml file.

Internals

Uses bounded model checking (BMC) or k-induction, combined with invariant inference and witness checking. Extends ESBMC to falsify or prove correctness of a given (safety) property for any depth without manual annotation of loops with invariants. Uses CPAchecker, Ultimate Automizer, PAGAI, PIPS