Related papers: Higher-Order MSL Horn Constraints
The monadic shallow linear Horn fragment is well-known to be decidable and has many application, e.g., in security protocol analysis, tree automata, or abstraction refinement. It was a long standing open problem how to extend the fragment…
Motivated by applications in automated verification of higher-order functional programs, we develop a notion of constrained Horn clauses in higher-order logic and a decision problem concerning their satisfiability. We show that, although…
We report on work in progress on automatic procedures for proving properties of programs written in higher-order functional languages. Our approach encodes higher-order programs directly as first-order SMT problems over Horn clauses. It is…
Higher-order constrained Horn clauses (HoCHC) are a semantically-invariant system of higher-order logic modulo theories. With semi-decidable unsolvability over a semi-decidable background theory, HoCHC is suitable for safety verification.…
We present initial limit Datalog, a new extensible class of constrained Horn clauses for which the satisfiability problem is decidable. The class may be viewed as a generalisation to higher-order logic (with a simple restriction on types)…
Building on the successes of satisfiability modulo theories (SMT), Bj{\o}rner et al. initiated a research programme advocating Horn constraints as a suitable basis for automatic program verification. The notion of first-order constrained…
We show how automatic tools for the verification of linear and branching time properties of procedural, multi-threaded, and functional programs as well as program synthesis can be naturally and uniformly seen as solvers of constraints in…
In this paper we show that checking satisfiability of a set of non-linear Horn clauses (also called a non-linear Horn clause program) can be achieved using a solver for linear Horn clauses. We achieve this by interleaving a program…
We present the derivation reduction problem for SLD-resolution, the undecidable problem of finding a finite subset of a set of clauses from which the whole set can be derived using SLD-resolution. We study the reducibility of various…
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…
There are two kinds of higher-order extensions of model checking: HORS model checking and HFL model checking. Whilst the former has been applied to automated verification of higher-order functional programs, applications of the latter have…
Verification problems of programs written in various paradigms (such as imperative, logic, concurrent, functional, and object-oriented ones) can be reduced to problems of solving Horn clause constraints on predicate variables that represent…
We present a simple resolution proof system for higher-order constrained Horn clauses (HoCHC) - a system of higher-order logic modulo theories - and prove its soundness and refutational completeness w.r.t. the standard semantics. As…
Linear constraints are the linear counterpart of Haskell's class constraints. Linearly typed parameters allow the programmer to control resources such as file handles and manually managed memory as linear arguments. Indeed, a linear type…
A number of first-order calculi employ an explicit model representation formalism for automated reasoning and for detecting satisfiability. Many of these formalisms can represent infinite Herbrand models. The first-order fragment of…
In recent years they have been numerous works that aim to automate relational verification. Meanwhile, although Constrained Horn Clauses (CHCs) empower a wide range of verification techniques and tools, they lack the ability to express…
Constrained Horn Clauses (CHCs) have conventionally been used as a low-level representation in formal verification. Most existing solvers use a diverse set of specialized techniques, including direct state space traversal or…
Constrained Horn Clauses (CHCs) are an intermediate program representation that can be generated by several verification tools, and that can be processed and solved by a number of Horn solvers. One of the main challenges when using CHCs in…
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…
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…