ESBMC v6.0: Verifying C Programs Using k-Induction and Invariant Inference - (Competition Contribution).
2019
ESBMC v6.0 employs a k-induction algorithm to both falsify and prove safety properties in C programs. We have developed a new interval-invariant generator that pre-processes the program, inferring invariants based on intervals and introducing them in the program as assumptions. Our experiments show that ESBMC v6.0 using k-induction can prove up to 7% more programs when the invariant generation is enabled.
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
7
References
25
Citations
NaN
KQI