This paper presents the ELDARICA version 2 model checker. Over the last years we have
been develo** and maintaining ELDARICA as a state-of-the-art solver for Horn clauses …

Program proving can be viewed as solving for unknown relations (such as loop invariants,
procedure summaries and so on) that occur in the logical verification conditions of a …

We present a decision procedure for a logic that combines (i) word equations over string
variables denoting words of arbitrary lengths, together with (ii) constraints on the length of …

We propose a method for automatically finding refinement types of higher-order function
programs. Our method is an extension of the Ice framework of Garg et al. for finding …

Differential privacy has emerged as a promising probabilistic formulation of privacy,
generating intense interest within academia and industry. We present a push-button …

One of the main challenges in software verification is efficient and precise compositional
analysis of programs with procedures and loops. Interpolation methods remains one of the …

We present VeriMAP, a tool for the verification of C programs based on the transformation of
constraint logic programs, also called constrained Horn clauses. VeriMAP makes use of …

We present a modular approach to automatic complexity analysis of integer programs.
Based on a novel alternation between finding symbolic time bounds for program parts and …

A Constrained Horn Clause (CHC) is a logical implication involving unknown predicates.
Systems of CHCs are widely used to verify programs with arbitrary loop structures …

We present a method for automatically generating verification conditions for a class of
imperative programs and safety properties. Our method is parametric with respect to the …