Back to Search
Start Over
An iterative approach to precondition inference using constrained Horn clauses
- Publication Year :
- 2018
- Publisher :
- arXiv, 2018.
-
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.<br />Comment: Paper presented at the 34nd International Conference on Logic Programming (ICLP 2018), Oxford, UK, July 14 to July 17, 2018 18 pages, LaTeX
- Subjects :
- FOS: Computer and information sciences
Computer Science - Logic in Computer Science
Mathematical optimization
Horn clause
Computer science
Inference
Program transformation
020207 software engineering
02 engineering and technology
Partial evaluation
Theoretical Computer Science
Precondition
Logic in Computer Science (cs.LO)
Program analysis
Computational Theory and Mathematics
Artificial Intelligence
Hardware and Architecture
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
0202 electrical engineering, electronic engineering, information engineering
020201 artificial intelligence & image processing
Software
Logic programming
Complement (set theory)
Subjects
Details
- Database :
- OpenAIRE
- Accession number :
- edsair.doi.dedup.....9995e47bfa0a969db8cc66efafd4e742
- Full Text :
- https://doi.org/10.48550/arxiv.1804.05989