ESBMC v6.0: Verifying C Programs Using k-Induction and Invariant Inference (Competition Contribution)

摘要

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.