Solving Horn Clauses on Inductive Data Types Without Induction
arXiv:1804.09007 · doi:10.1017/S1471068418000157
Abstract
We address the problem of verifying the satisfiability of Constrained Horn Clauses (CHCs) based on theories of inductively defined data structures, such as lists and trees. We propose a transformation technique whose objective is the removal of these data structures from CHCs, hence reducing their satisfiability to a satisfiability problem for CHCs on integers and booleans. We propose a transformation algorithm and identify a class of clauses where it always succeeds. We also consider an extension of that algorithm, which combines clause transformation with reasoning on integer constraints. Via an experimental evaluation we show that our technique greatly improves the effectiveness of applying the Z3 solver to CHCs. We also show that our verification technique based on CHC transformation followed by CHC solving, is competitive with respect to CHC solvers extended with induction. This paper is under consideration for acceptance in TPLP.
Paper presented at the 34nd International Conference on Logic Programming (ICLP 2018), Oxford, UK, July 14 to July 17, 2018. 22 pages, LaTeX
References in corpus (3)
Cited by in corpus (11)
- Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates
- Verifying Catamorphism-Based Contracts using Constrained Horn Clauses
- Lemma Generation for Horn Clause Satisfiability: A Preliminary Study
- Proving Properties of Sorting Programs: A Case Study in Horn Clause Verification
- Program Specialization as a Tool for Solving Word Equations
- Contract Strengthening through Constrained Horn Clause Verification
- Symbolic Automatic Relations and Their Applications to SMT and CHC Solving
- An Overview of the HFL Model Checking Project
- Solving Constrained Horn Clauses over ADTs by Finite Model Finding
- On Solving Word Equations via Program Transformation
- Transformational Verification of Quicksort