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

Format:

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

Links

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

Last commit date

9 January 2019

Related papers

https://doi.org/10.1007/978-3-662-54580-5_23 (TACAS '17)

Last publication date

31 March 2017

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.