Improving Counterexample Quality from Failed Program Verification

TL;DR

This paper presents CEAM, a method to extract and simplify understandable counterexamples from failed program proofs, aiding developers in diagnosing verification issues.

Contribution

It introduces CEAM, a novel approach that transforms and minimizes counterexamples to improve clarity in failed software verification proofs.

Findings

CEAM produces clearer, more understandable counterexamples.

The approach effectively simplifies counterexamples by minimizing integer values.

Implementation in AutoProof demonstrates practical utility.

Abstract

In software verification, a successful automated program proof is the ultimate triumph. The road to such success is, however, paved with many failed proof attempts. The message produced by the prover when a proof fails is often obscure, making it very hard to know how to proceed further. The work reported here attempts to help in such cases by providing immediately understandable counterexamples. To this end, it introduces an approach called Counterexample Extraction and Minimization (CEAM). When a proof fails, CEAM turns the counterexample model generated by the prover into a a clearly understandable version; it can in addition simplify the counterexamples further by minimizing the integer values they contain. We have implemented the CEAM approach as an extension to the AutoProof verifier and demonstrate its application to a collection of examples.