Abstract
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 extension 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.
Original language | English |
---|---|
Title of host publication | Programming Languages and Systems |
Subtitle of host publication | 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings |
Publisher | Springer Berlin Heidelberg |
Pages | 451-471 |
Number of pages | 21 |
Volume | 7792 |
ISBN (Electronic) | 978-3-642-37036-6 |
ISBN (Print) | 978-3-642-37036-6 |
DOIs | |
Publication status | Published - 2013 |