Analysis and Transformation of Constrained Horn Clauses for Program Verification
From MaRDI portal
Abstract: This paper surveys recent work on applying analysis and transformation techniques that originate in the field of constraint logic programming (CLP) to the problem of verifying software systems. We present 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. Then, we describe static analysis techniques for CHCs that may be used for inferring relevant program properties, such as loop invariants. We also give an overview of some transformation techniques based on specialisation and fold/unfold rules, which are useful for improving the effectiveness of CHC satisfiability tools. Finally, we discuss future developments in applying these techniques.
Recommendations
- Static analysis, abstract interpretation and verification in (constraint logic) programming
- RustHorn: CHC-based verification for Rust programs
- Solving Horn clauses on inductive data types without induction
- Relational verification through Horn clause transformation
- Horn clause solvers for program verification
Cites work
- A bottom-up polymorphic type inference in logic programming
- A decompositional approach for computing least fixed-points of datalog programs with \(\mathcal Z\)-counters
- A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs
- A general framework for static profiling of parametric resource usage
- A lattice-theoretical fixpoint theorem and its applications
- A Transformation System for Developing Recursive Programs
- A transformational approach to parametric accumulated-cost static profiling
- Abstract interpretation and application to logic programs
- Abstract interpretation based on Alexander Templates
- Abstract interpretation of logic programs using magic transformations
- Abstract Interpretation with Specialized Definitions
- Abstract interpretation: a kind of magic
- Abstract multiple specialization and its application to program parallelization
- An axiomatic basis for computer programming
- An efficient SMT solver for string constraints
- An integrated approach to assertion-based random testing in Prolog
- An iterative approach to precondition inference using constrained Horn clauses
- An overview of Ciao and its design philosophy
- An overview of the K semantic framework
- Analysis of Linear Hybrid Systems in CLP
- Analyzing logic programs using “prop”-ositional logic programs and a magic wand
- Automating induction for solving Horn clauses
- BEYOND TAMAKI-SATO STYLE UNFOLD/FOLD TRANSFORMATIONS FOR NORMAL LOGIC PROGRAMS
- Bottom-up abstract interpretation of logic programs
- Closed-form upper bounds in static cost analysis
- Coinductive Logic Programming and Its Applications
- Compile-time derivation of variable dependency using abstract interpretation
- Concolic testing in CLP
- Conjunctive partial deduction: foundations, control, algorithms, and experiments
- Constraint-based deductive model checking
- Control-flow refinement by partial evaluation, and its application to termination and cost analysis
- Controlling polyvariance for specialization-based verification
- Convex hull abstractions in specialization of CLP programs
- Cost analysis of object-oriented bytecode programs
- Counterexample-guided abstraction refinement for symbolic model checking
- Decidable logics combining heap structures and data
- Deciding floating-point logic with abstract conflict driven clause learning
- Decision procedures for flat array properties
- Deforestation: Transforming programs to eliminate trees
- Dynamic partial-order reduction for model checking software
- Efficient generation of test data structures using constraint logic programming and program transformation
- Exploiting goal independence in the analysis of logic programs
- Failure tabled constraint logic programming by interpolation
- Generalization strategies for the verification of infinite state systems
- Generalized property directed reachability
- Grammar-related transformations of logic programs
- Horn clause computability
- Horn clause solvers for program verification
- Horn clause verification with convex polyhedral abstraction and tree automata-based refinement
- Horn clauses as an intermediate representation for program analysis and transformation
- scientific article; zbMATH DE number 1617330 (Why is no real title available?)
- scientific article; zbMATH DE number 1615252 (Why is no real title available?)
- scientific article; zbMATH DE number 1615263 (Why is no real title available?)
- scientific article; zbMATH DE number 1696790 (Why is no real title available?)
- scientific article; zbMATH DE number 1696815 (Why is no real title available?)
- scientific article; zbMATH DE number 4035108 (Why is no real title available?)
- scientific article; zbMATH DE number 43398 (Why is no real title available?)
- scientific article; zbMATH DE number 108368 (Why is no real title available?)
- scientific article; zbMATH DE number 3467028 (Why is no real title available?)
- scientific article; zbMATH DE number 1234104 (Why is no real title available?)
- scientific article; zbMATH DE number 1257634 (Why is no real title available?)
- scientific article; zbMATH DE number 512885 (Why is no real title available?)
- scientific article; zbMATH DE number 1142320 (Why is no real title available?)
- scientific article; zbMATH DE number 1973221 (Why is no real title available?)
- scientific article; zbMATH DE number 1538039 (Why is no real title available?)
- scientific article; zbMATH DE number 1368925 (Why is no real title available?)
- scientific article; zbMATH DE number 7453190 (Why is no real title available?)
- scientific article; zbMATH DE number 7453201 (Why is no real title available?)
- scientific article; zbMATH DE number 236855 (Why is no real title available?)
- scientific article; zbMATH DE number 5194318 (Why is no real title available?)
- scientific article; zbMATH DE number 3248792 (Why is no real title available?)
- scientific article; zbMATH DE number 3336816 (Why is no real title available?)
- ICE-based refinement type discovery for higher-order functional programs
- Improving reachability analysis of infinite state systems by specialization
- Incremental analysis of logic programs with assertions and open predicates
- Induction for SMT solvers
- Inference rules for proving the equivalence of recursive procedures
- Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor)
- Interval-based resource usage verification by translation into Horn clauses and an application to energy consumption
- Interval-based resource usage verification: formalization and prototype
- Isabelle/HOL. A proof assistant for higher-order logic
- Linear resolution with selection function
- Logic program specialisation through partial deduction: Control issues
- Logic programming and negation: A survey
- Mechanized semantics for the clight subset of the C language
- Mixtus: An automatic partial evaluator for full Prolog
- Model checking
- Newtonian program analysis
- On certain axiomatizations of arithmetic of natural and integer numbers
- On the implementation of the probabilistic logic programming language ProbLog
- Optimized algorithms for incremental analysis of logic programs
- Partial evaluation in logic programming
- Polyvariant mixed computation for analyzer programs
- Precise interprocedural dataflow analysis with applications to constant propagation
- Predicate pairing for program verification
- Predicate pairing with abstraction for relational verification
- Probabilistic Horn clause verification
- Program Development in Computational Logic
- Programming Languages and Systems
- Proving properties of co-logic programs by unfold/fold transformations
- Proving theorems by program transformation
- Refinement of Trace Abstraction
- Relational cost analysis
- Relational verification through Horn clause transformation
- Relational verification via invariant-guided synchronization
- Removing algebraic data types from constrained Horn clauses using difference predicates
- Removing Superfluous Versions in Polyvariant Specialization of Prolog Programs
- Resource usage analysis of logic programs via abstract interpretation using sized types
- SAT modulo linear arithmetic for solving polynomial constraints
- SAT-Based Model Checking without Unrolling
- Satisfiability modulo theories
- Semantics and controllability of time-aware business processes
- Simple relational correctness proofs for static analyses and program transformations
- Simplification by Cooperating Decision Procedures
- SMT-based model checking for recursive programs
- Software model checking
- Solving Horn clauses on inductive data types without induction
- Solving non-linear arithmetic
- Synchronizing constrained Horn clauses
- Syntax-guided termination analysis
- Test case generation for object-oriented imperative languages in CLP
- Test case generation of actor systems
- The Alexander Method - a technique for the processing of recursive axioms in deductive databases
- The automation of proof by mathematical induction
- The loop absorption and the generalization strategies for the development of logic programs and partial deduction
- The MathSAT5 SMT solver
- The semantics of constraint logic programs1Note that reviewing of this paper was handled by the Editor-in-Chief.1
- Theory and practice of constraint handling rules
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- TRACER: a symbolic execution tool for verification
- Transformation of logic programs: Foundations and techniques
- Transformations of CLP modules
- Tree dimension in verification of constrained Horn clauses
- Unfold/fold transformation of stratified programs
- Unfolding--definition--folding, in this order, for avoiding unnecessary variables in logic programs
- Why3 -- where programs meet provers
Cited in
(10)- A Transformational Approach for Proving Properties of the CHR Constraint Store
- Horn clauses as an intermediate representation for program analysis and transformation
- Proving correctness of imperative programs by linearizing constrained Horn clauses
- Towards a dereversibilizer: fewer asserts, statically
- scientific article; zbMATH DE number 7806141 (Why is no real title available?)
- scientific article; zbMATH DE number 7806143 (Why is no real title available?)
- Symbolic Model Construction for Saturated Constrained Horn Clauses
- Runtime repeated recursion unfolding in CHR: a just-in-time online program optimization strategy that can achieve super-linear speedup
- CHC-COMP 2023: competition report
- Catamorphic abstractions for constrained Horn clause satisfiability
This page was built for publication: Analysis and Transformation of Constrained Horn Clauses for Program Verification
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6063893)
