ABSTRACT. In this talk, we present our recent and ongoing work on constraint solving for verification of higher-order functional programs, where we address two important classes of specifications: (1) relational specifications and (2) dependent temporal specifications. These classes impose a new challenge: validity checking of first-order formulas with least and greatest fixpoints respectively for inductive and coinductive predicates, which generalizes existing variants of constrained Horn clause (CHC) solving.

The former class of relational specifications includes functional equivalence, associativity, commutativity, distributivity, monotonicity, idempotency, and non-interference, whose verification often boils down to inferring mutual invariants among inputs and outputs of multiple function calls. To this end, we present a novel CHC solving method based on inductive theorem proving: the method reduces CHC solving to validity checking of first-order formulas with least fixpoints for inductive predicates, which are then checked by induction on the derivation of the predicates. The method thus enables relational verification by expressing and checking mutual invariants as induction hypotheses.

The latter class of dependent temporal specifications is used to constrain (possibly infinite) event sequences generated by the target program. We express temporal specifications as first-order formulas over finite and infinite strings that encode event sequences. The use of first-order formulas allows us to express temporal specifications that depend on program values, so that we can specify input-dependent temporal behavior of the target program. Furthermore, we use least and greatest fixpoints to respectively model finite and infinite event sequences generated by the target program. To solve such fixpoint constraints, we present a novel deductive system consisting of rules for soundly eliminating fixpoints via invariants and well-founded relations.

ABSTRACT. Dynamically typed languages, like Erlang, allow developers to quickly write programs without explicitly providing any type information on expressions or function definitions. However, this feature makes dynamic languages less reliable, because many runtime errors would be easily caught in statically typed languages. Besides, adding concurrency to the mix leads to a programming language where some runtime errors only appear for a particular execution of the program. In this paper, we present our preliminary work 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. In particular, by using Constraint Logic Programming, we develop an interpreter that, given an Erlang program and a symbolic input, returns answer constraints that represent sets of concrete data for which the Erlang program will incur in a runtime error.

ABSTRACT. Recursion-free Constrained Horn Clauses (CHCs) are logic-programming problems that can model safety properties of programs with bounded iteration and recursion. In addition, many CHC solvers which handle recursive systems reduce their inputs to a series of recursion-free CHC systems that can each be solved efficiently.

In this paper, we define a novel class of recursion-free systems, named Clause-Dependence Disjoint (CDD), that generalizes classes defined in previous work. The advantage of this class is that many CDD systems are smaller than systems which express the same constraints but are part of a different class. This advantage in size allows CDD systems to be solved more efficiently than their counterparts in other classes. Based on the class of CDD systems, we implemented a CHC solver named Shara. Shara solves arbitrary CHC systems by reducing the input to a series of CDD systems. Our evaluation indicates that Shara outperforms state-of-the-art implementations in many practical cases.

ABSTRACT. We present a recursive formulation of the Horn algorithm for deciding the satisfiability of propositional clauses. The usual presentations in imperative pseudo-code are informal and not suitable for simple proofs of its main properties. By defining the algorithm as a recursive function (computing a least fixed-point), we achieve: 1) a concise, yet rigorous, formalisation; 2) a clear form of visualising executions of the algorithm, step-by-step; 3) precise results, simple to state and with clean inductive proofs.

ABSTRACT. Coinduction occurs in two guises in Horn clause logic: in proofs of self-referencing properties and relations, and in proofs involving construction of (possibly irregular) infinite data. Both instances of coinductive reasoning appeared in the literature before, but a systematic analysis of these two kinds of proofs and of their relation was lacking. We propose a general proof-theoretic framework for handling both kinds of coinduction arising in Horn clause logic. To this aim, we propose a coinductive extension of Miller et al's framework of uniform proofs and prove its soundness relative to coinductive models of Horn clause logic.

ABSTRACT. I will introduce the notion of tree dimension and how it can be used in the verification of constrained Horn clauses. The dimension of a tree is a numerical measure of its branching complexity and the concept here applies to Horn clause derivation trees. I will show how to reason about the dimensions of derivations and how to filter out derivation trees below or above some dimension bound using clause transformations.

I will then present algorithms using these constructions to decompose a constrained Horn clauses verification problem. Finally I will report on implementations and experimental results.

ABSTRACT. We show that Cubicle,an SMT-based infinite-state model checker, can be applied as a verification engine for GLog, a logic-based specification language for topology-sensitive distributed protocols with asynchronous communication. Existential coverability queries in GLog can be translated into verification judgements in Cubicle by encoding relational updates rules as unbounded array transitions. We apply the resulting framework to automatically verify a distributed.  version of the Dining Philosopher mutual exclusion protocol formulated for an arbitrary number of nodes and communication buffers.

ABSTRACT. New this year will be the CHC competition CHC-COMP, which will compare state-of-the-art tools for CHC solving with respect to performance and effectiveness on a set of publicly available benchmarks. More informations can be found at https://chc-comp.github.io/.