# An iterative approach to precondition inference using constrained Horn clauses

@article{Kafle2018AnIA, title={An iterative approach to precondition inference using constrained Horn clauses}, author={Bishoksan Kafle and John P. Gallagher and Graeme Gange and Peter Schachte and Harald S{\o}ndergaard and Peter James Stuckey}, journal={Theory and Practice of Logic Programming}, year={2018}, volume={18}, pages={553 - 570} }

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… Expand

#### Topics from this paper

#### 11 Citations

Precondition Inference via Partitioning of Initial States

- Computer Science
- ArXiv
- 2018

This work presents a novel iterative method for automatically deriving sufficient preconditions for safety and unsafety of programs which introduces a new dimension of modularity. Expand

Transformation-Enabled Precondition Inference

- Computer Science
- Theory and Practice of Logic Programming
- 2021

An experimental evaluation of the novel iterative method for automatically deriving preconditions for the safety and unsafety of programs shows that it can infer precise precond conditions that are not possible using previous methods. Expand

Analysis and Transformation of Constrained Horn Clauses for Program Verification

- Computer Science
- ArXiv
- 2021

Specialisation-based techniques for translating verification problems for different programming languages, and in general software systems, into satisfiability problems for constrained Horn clauses (CHCs), a term that has become popular in the verification field to refer to CLP programs. Expand

Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis

- Computer Science
- Theory and Practice of Logic Programming
- 2019

This paper explores the use of partial evaluation of Horn clauses as a general-purpose technique for control-flow refinement for integer transitions systems and uses a partial evaluation algorithm incorporating property-based abstraction to prove termination and to infer complexity of challenging programs that cannot be handled by state-of-the-art tools. Expand

Polyvariant Program Specialisation with Property-based Abstraction

- Computer Science
- VPT@Programming
- 2019

Property-based abstraction is shown to be a flexible method of controlling polyvariance in program specialisation in a standard online specialisation algorithm and its application in control flow refinement, verification, termination analysis and dimension-based specialisation is discussed. Expand

Resource Analysis driven by (Conditional) Termination Proofs

- Computer Science
- Theory and Practice of Logic Programming
- 2019

A novel approach to resource analysis that is driven by the result of a termination analysis that produces a linearly-bounded CRS (LB-CRS), which is composed of cost functions that are guaranteed to be locally bounded by linear ranking functions and thus greatly simplify the process of CRS solving. Expand

Control-Flow Refinment via Partial Evaluation

- 2018

Its execution has two implicit phases: in the first one, variable y is incremented until it reaches the value of z, and in the second phase the value of x is decremented until it reaches the value 0.… Expand

Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction

- Computer Science, Engineering
- Fundam. Informaticae
- 2021

This work proposes a semi-algorithm using refinement of trace abstractions to solve both the reachability verification problem and the parameter synthesis problem for real-time programs. Expand

Bounded Symbolic Execution for Runtime Error Detection of Erlang Programs

- Computer Science
- HCVS
- 2018

A preliminary work is presented on a tool that, by using the well-known techniques of metaprogramming and symbolic execution, can be used to perform bounded verification of Erlang programs. Expand

Postprocessing of static analysis alarms

- Computer Science
- 2020

The final author version and the galley proof are versions of the publication after peer review that features the final layout of the paper including the volume, issue and page numbers. Expand

#### References

SHOWING 1-10 OF 43 REFERENCES

Program verification via iterated specialization

- Computer Science
- Sci. Comput. Program.
- 2014

This work presents a method for verifying properties of imperative programs by using techniques based on the specialization of constraint logic programs (CLP), and improves the precision of program verification with respect to state-of-the-art software model checkers. Expand

Precondition Inference from Intermittent Assertions and Application to Contracts on Collections

- Computer Science
- VMCAI
- 2011

This work defines precisely and formally the contract inference problem from intermittent assertions inserted in the code by the programmer and introduces new abstract interpretation-based methods to automatically infer both the static contract precondition of a method/procedure and the code to check it at runtime on scalar and collection variables. Expand

Constraint Specialisation in Horn Clause Verification

- Computer Science
- PEPM
- 2015

This work uses abstract interpretation to compute a model of a query-answer transformation of a given set of clauses and a goal, which is to propagate the constraints from the goal top-down and propagate answer constraints bottom-up. Expand

Path invariants

- Computer Science
- PLDI '07
- 2007

The method handles loops without unrolling and infers abstractions that involve universal quantification and naturally incorporates disjunctive reasoning, and uses path invariants for abstraction refinement in order to remove all infeasible error computations that are represented by a path program. Expand

Semantics-based generation of verification conditions via program specialization

- Computer Science
- Sci. Comput. Program.
- 2017

It is proved that automated verification of programs from a formal definition of the operational semantics is indeed feasible in practice, and that the verification condition generation takes a number of transformation steps that is linear with respect to the size of the imperative program to be verified. Expand

Combining Forward and Backward Abstract Interpretation of Horn Clauses

- Computer Science
- SAS
- 2017

This work introduces a new backward collecting semantics, suitable for alternating forward and backward abstract interpretation of Horn clauses, and shows how the alternation can be used to prove unreachability of the goal and how every subsequent run of an analysis yields a refined model of the system. Expand

Analysing Logic Programs by Reasoning Backwards

- Computer Science
- Program Development in Computational Logic
- 2004

This paper reviews various backwards analyses that have been proposed for logic programs, identifying common threads in these techniques and suggesting some suggestions for research in backwards analysis for logic program development. Expand

Automatically Refining Abstract Interpretations

- Mathematics, Computer Science
- TACAS
- 2008

Three techniques to automatically refine abstract interpretations to reduce false errors are presented, including a new operator called interpolated widen, which automatically recovers precision lost due to widen, a new way to handle disjunctions that arise due to refinement, and a new refinement algorithm, which refines abstract interpretations that use the join operator to merge abstract states at join points. Expand

The Semantics of Constraint Logic Programs

- Computer Science, Mathematics
- J. Log. Program.
- 1998

The semantic foundations of CLP in a self-contained and complete package is presented, giving new and complete proofs for the main lemmas and clarified which theorems depend on conditions such as solution compactness, satisfaction completeness and independence of constraints. Expand

A Practical and Complete Approach to Predicate Refinement

- Computer Science, Mathematics
- TACAS
- 2006

This work presents a practical method of predicate selection that is complete in the above sense, based on interpolation and uses a “split prover”, somewhat in the style of structure-based provers used in artificial intelligence. Expand