Counterexample-guided Precondition Inference
Nassim Seghir ( University of Oxford )
- 11:30 6th March 2013 ( week 8, Hilary Term 2013 )051
The precondition for an assertion inside a procedure is useful
for understanding, verifying and debugging programs. As the procedure
might be used in multiple calling-contexts within a program, the precondition
should be sufficiently general to enable re-use. We present an ex-
tension of counterexample-guided abstraction refinement (CEGAR) for
automated precondition inference. Starting with an over-approximation
of both the set of safe and unsafe states, we iteratively refine them until
they become disjoint. The resulting precondition is then necessary and
sufficient for the validity of the assertion, which prevents false alarms.
We have implemented our approach in a tool called P-Gen. We present
experimental results on string and array-manipulating programs.