Related papers: Automating Induction for Solving Horn Clauses
The functional properties of a program are often specified by providing a contract for each of its functions. A contract of a function consists of a pair of formulas, called a precondition and a postcondition, which, respectively, should…
We propose a procedure for automated implicit inductive theorem proving for equational specifications made of rewrite rules with conditions and constraints. The constraints are interpreted over constructor terms (representing data values),…
We consider constrained Horn clause solving from the more general point of view of solving formula equations. Constrained Horn clauses correspond to the subclass of Horn formula equations. We state and prove a fixed-point theorem for Horn…
We establish proof-theoretic, constructive and coalgebraic foundations for proof search in coinductive Horn clause theories. Operational semantics of coinductive Horn clause resolution is cast in terms of coinductive uniform proofs; its…
Prolog is a well known declarative programming language based on propositional Horn formulas. It is useful in various areas, including artificial intelligence, automated theorem proving, mathematical logic and so on. An active research area…
We propose a new type-theoretic approach to SLD-resolution and Horn-clause logic programming. It views Horn formulas as types, and derivations for a given query as a construction of the inhabitant (a proof-term) for the type given by the…
We address the problem of verifying that the functions of a program meet their contracts, specified by pre/postconditions. We follow an approach based on constrained Horn clauses (CHCs) by which the verification problem is reduced to the…
We address the problem of checking the satisfiability of Constrained Horn Clauses (CHCs) defined on Algebraic Data Types (ADTs), such as lists and trees. We propose a new technique for transforming CHCs defined on ADTs into CHCs where the…
This paper tackles the problem of the existence of solutions for recursive systems of Horn clauses with second-order variables interpreted as integer relations, and harnessed by quantifier-free difference bounds arithmetic. We start by…
Program verification and synthesis frameworks that allow one to customize the language in which one is interested typically require the user to provide a formally defined semantics for the language. Because writing a formal semantics can be…
We present a verification technique for program safety that combines Iterated Specialization and Interpolating Horn Clause Solving. Our new method composes together these two techniques in a modular way by exploiting the common Horn Clause…
This paper presents a verification framework based on a new class of predicate Constraint Satisfaction Problems called pCSP where constraints are represented as clauses modulo first-order theories over function variables and predicate…
Constrained Horn Clauses (CHCs) are often used in automated program verification. Thus, techniques for (dis-)proving satisfiability of CHCs are a very active field of research. On the other hand, acceleration techniques for computing…
Several techniques and tools have been developed for verification of properties expressed as Horn clauses with constraints over a background theory (CHC). Current CHC verification tools implement intricate algorithms and are often limited…
We present a compositional SMT-based algorithm for safety of procedural C programs that takes the heap into consideration as well. Existing SMT-based approaches are either largely restricted to handling linear arithmetic operations and…
We propose a hybrid-dynamic first-order logic as a formal foundation for specifying and reasoning about reconfigurable systems. As the name suggests, the formalism we develop extends (many-sorted) first-order logic with features that are…
We present HornStr, the first solver for invariant synthesis for Regular Model Checking (RMC) with the specification provided in the SMT-LIB 2.6 theory of strings. It is well-known that invariant synthesis for RMC subsumes various important…
An inductive inference system for proving validity of formulas in the initial algebra $T_{\mathcal{E}}$ of an order-sorted equational theory $\mathcal{E}$ is presented. It has 20 inference rules, but only 9 of them require user interaction;…
Relational verification is a technique that aims at proving properties that relate two different program fragments, or two different program runs. It has been shown that constrained Horn clauses (CHCs) can effectively be used for relational…
Despite decades of research, there are still a number of concepts commonly found in software programs that are considered challenging for verification: among others, such concepts include concurrency, and the compositional analysis of…