An iterative approach to precondition inference using constrained Horn clauses
From MaRDI portal
Abstract: We present a method for automatic inference of conditions on the initial states of a program that guarantee that the safety assertions in the program are not violated. Constrained Horn clauses (CHCs) are used to model the program and assertions in a uniform way, and we use standard abstract interpretations to derive an over-approximation of the set of unsafe initial states. The precondition then is the constraint corresponding to the complement of that set, under-approximating the set of safe initial states. This idea of complementation is not new, but previous attempts to exploit it have suffered from the loss of precision. Here we develop an iterative specialisation algorithm to give more precise, and in some cases optimal safety conditions. The algorithm combines existing transformations, namely constraint specialisation, partial evaluation and a trace elimination transformation. The last two of these transformations perform polyvariant specialisation, leading to disjunctive constraints which improve precision. The algorithm is implemented and tested on a benchmark suite of programs from the literature in precondition inference and software verification competitions.
Recommendations
Cites work
- Abstract interpretation and application to logic programs
- An overview of Ciao and its design philosophy
- Computer aided verification. 21st international conference, CAV 2009, Grenoble, France, June 26--July 2, 2009. Proceedings
- Computer aided verification. 24th international conference, CAV 2012, Berkeley, CA, USA, July 7--13, 2012. Proceedings
- Computer aided verification. 9th international conference, CAV'97, Haifa, Israel, June 22--25, 1997. Proceedings
- Counterexample-guided abstraction refinement for symbolic model checking
- Horn clause verification with convex polyhedral abstraction and tree automata-based refinement
- scientific article; zbMATH DE number 236855 (Why is no real title available?)
- Inferring sufficient conditions with backward polyhedral under-approximations
- Integrated Formal Methods
- Program Development in Computational Logic
- Reachability problems. 11th international workshop, RP 2017, London, UK, September 7--9, 2017. Proceedings
- Static analysis. 24th international symposium, SAS 2017, New York, NY, USA, August 30 -- September 1, 2017. Proceedings
- Static analysis. 5th international symposium, SAS '98, Pisa, Italy, September 14--16, 1998. Proceedings
- The octagon abstract domain
- The semantics of constraint logic programs1Note that reviewing of this paper was handled by the Editor-in-Chief.1
- Tools and Algorithms for the Construction and Analysis of Systems
- Tools and algorithms for the construction and analysis of systems. 14th international conference, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29--April 6, 2008. Procee
- Tools and algorithms for the construction and analysis of systems. 19th international conference, TACAS 2013, held as part of the European joint conferences on theory and practice of software, ETAPS 2013, Rome, Italy, March 16--24, 2013. Proceedings
- Verification, model checking, and abstract interpretation. 12th international conference, VMCAI 2011, Austin, TX, USA, January 23--25, 2011. Proceedings
- Verification, model checking, and abstract interpretation. 9th international conference, VMCAI 2008, San Francisco, USA, January 7--9, 2008. Proceedings
Cited in
(10)- Bounded symbolic execution for runtime error detection of Erlang programs
- Verification and parameter synthesis for real-time programs using refinement of trace abstraction
- Resource analysis driven by (conditional) termination proofs
- Control-flow refinement by partial evaluation, and its application to termination and cost analysis
- Inferring sufficient conditions with backward polyhedral under-approximations
- Counterexample-guided precondition inference
- Transformation-Enabled Precondition Inference
- Analysis and Transformation of Constrained Horn Clauses for Program Verification
- Discovering implied constraints in precedence graphs with alternatives
- A query-based constraint acquisition approach for enhanced precision in program precondition inference
This page was built for publication: An iterative approach to precondition inference using constrained Horn clauses
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4559813)
