Counterexample-Guided Precondition Inference

Mohamed Nassim Seghir, Daniel Kroening

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 languageEnglish
Title of host publicationProgramming Languages and Systems
Subtitle of host publication22nd 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
PublisherSpringer Berlin Heidelberg
Pages451-471
Number of pages21
Volume7792
ISBN (Electronic)978-3-642-37036-6
ISBN (Print)978-3-642-37036-6
DOIs
Publication statusPublished - 2013

Fingerprint

Dive into the research topics of 'Counterexample-Guided Precondition Inference'. Together they form a unique fingerprint.

Cite this