DepthK: A k-induction verifier based on invariant inference for C programs
DepthK is a software verification tool that employs a proof by induction algorithm that combines k-induction with invariant inference. In order to efficiently and effectively verify and falsify safety properties in C programs, DepthK infers program invariants using polyhedral constraints. Experiment...
Main Authors: | , , , , |
---|---|
Format: | Conference item |
Published: |
Springer, Berlin, Heidelberg
2017
|