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 show that Cubicle,anSMT-basedinfinite-statemodel 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 arbi- trary number of nodes and communication buffers.

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. 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. 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.