ESBMC v6.0: Verifying C Programs Using k-Induction and Invariant Inference

作者：Mikhail R. Gadelha, Felipe R. Monteiro, Lucas C. Cordeiro, Denis A. Nicole · 发表于：Lecture notes in computer science · 年份：2019 · DOI：10.1007/978-3-030-17502-3_15 · 被引用次数：56 · 研究领域：Formal Methods in Verification、Security and Verification in Computing、Software Testing and Debugging Techniques

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.