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

Type of tool

Model checker

Expected input


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.


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
C Model checking


Repository: https://github.com/hbgit/depthk/

Related papers

DepthK: A k-Induction Verifier Based on Invariant Inference for C Programs (TACAS '17)

Last publication date

31 March 2017

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.