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
|