Fabio Fioravanti

Emanuele De Angelis, Fabio Fioravanti, Maria Chiara Meo et al.

Assumption-based Argumentation (ABA) is a well-established form of structured argumentation. ABA frameworks with an underlying atomic language are widely studied, but their applicability is limited by a representational restriction to ground (variable-free) arguments and attacks built from propositional atoms. In this paper, we lift this restriction and propose a novel notion of constrained ABA (CABA), whose components, as well as arguments built from them, may include constrained variables, ranging over possibly infinite domains. We define non-ground semantics for CABA, in terms of various notions of non-ground attacks. We show that the new semantics conservatively generalise standard ABA semantics.

Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi et al.

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 verification by applying a CHC transformation, called predicate pairing, which allows the CHC solver to infer relations among arguments of different predicates. In this paper we study how the effects of the predicate pairing transformation can be enhanced by using various abstract domains based on linear arithmetic (i.e., the domain of convex polyhedra and some of its subdomains) during the transformation. After presenting an algorithm for predicate pairing with abstraction, we report on the experiments we have performed on over a hundred relational verification problems by using various abstract domains. The experiments have been performed by using the VeriMAP transformation and verification system, together with the Parma Polyhedra Library (PPL) and the Z3 solver for CHCs.

Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi et al.

It is well-known that the verification of partial correctness properties of imperative programs can be reduced to the satisfiability problem for constrained Horn clauses (CHCs). However, state-of-the-art solvers for CHCs (CHC solvers) based on predicate abstraction are sometimes unable to verify satisfiability because they look for models that are definable in a given class A of constraints, called A-definable models. We introduce a transformation technique, called Predicate Pairing (PP), which is able, in many interesting cases, to transform a set of clauses into an equisatisfiable set whose satisfiability can be proved by finding an A-definable model, and hence can be effectively verified by CHC solvers. We prove that, under very general conditions on A, the unfold/fold transformation rules preserve the existence of an A-definable model, i.e., if the original clauses have an A-definable model, then the transformed clauses have an A-definable model. The converse does not hold in general, and we provide suitable conditions under which the transformed clauses have an A-definable model iff the original ones have an A-definable model. Then, we present the PP strategy which guides the application of the transformation rules with the objective of deriving a set of clauses whose satisfiability can be proved by looking for A-definable models. PP introduces a new predicate defined by the conjunction of two predicates together with some constraints. We show through some examples that an A-definable model may exist for the new predicate even if it does not exist for its defining atomic conjuncts. We also present some case studies showing that PP plays a crucial role in the verification of relational properties of programs (e.g., program equivalence and non-interference). Finally, we perform an experimental evaluation to assess the effectiveness of PP in increasing the power of CHC solving.

Emanuele De Angelis, Fabio Fioravanti, Maria Chiara Meo et al.

We present a method for verifying properties of time-aware business processes, that is, business process where time constraints on the activities are explicitly taken into account. Business processes are specified using an extension of the Business Process Modeling Notation (BPMN) and durations are defined by constraints over integer numbers. The definition of the operational semantics is given by a set OpSem of constrained Horn clauses (CHCs). Our verification method consists of two steps. (Step 1) We specialize OpSem with respect to a given business process and a given temporal property to be verified, whereby getting a set of CHCs whose satisfiability is equivalent to the validity of the given property. (Step 2) We use state-of-the-art solvers for CHCs to check the satisfiability of such sets of clauses. We have implemented our verification method using the VeriMAP transformation system, and the Eldarica and Z3 solvers for CHCs.

Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi et al.

Verification conditions (VCs) are logical formulas whose satisfiability guarantees program correctness. We consider VCs in the form of constrained Horn clauses (CHC) which are automatically generated from the encoding of (an interpreter of) the operational semantics of the programming language. VCs are derived through program specialization based on the unfold/fold transformation rules and, as it often happens when specializing interpreters, they contain unnecessary variables, that is, variables which are not required for the correctness proofs of the programs under verification. In this paper we adapt to the CHC setting some of the techniques that were developed for removing unnecessary variables from logic programs, and we show that, in some cases, the application of these techniques increases the effectiveness of Horn clause solvers when proving program correctness.

Emanuele De Angelis, Fabio Fioravanti, Jorge A. Navas et al.

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 representation of the verification problem. The Iterated Specialization verifier transforms an initial set of verification conditions by using unfold/fold equivalence preserving transformation rules. During transformation, program invariants are discovered by applying widening operators. Then the output set of specialized verification conditions is analyzed by an Interpolating Horn Clause solver, hence adding the effect of interpolation to the effect of widening. The specialization and interpolation phases can be iterated, and also combined with other transformations that change the direction of propagation of the constraints (forward from the program preconditions or backward from the error conditions). We have implemented our verification technique by integrating the VeriMAP verifier with the FTCLP Horn Clause solver, based on Iterated Specialization and Interpolation, respectively. Our experimental results show that the integrated verifier improves the precision of each of the individual components run separately.

Nikolaj Bjørner, Fabio Fioravanti, Andrey Rybalchenko et al.

This volume contains the proceedings of HCVS 2014, the First Workshop on Horn Clauses for Verification and Synthesis which was held on July 17, 2014 in Vienna, Austria as a satellite event of the Federated Logic Conference (FLoC) and part of the Vienna Summer of Logic (VSL 2014). HCVS 2014 was affiliated to the 26th International Conference on Computer Aided Verification (CAV 2014) and to the 30th International Conference on Logic Programming (ICLP 2014). Most Program Verification and Synthesis problems of interest can be modeled directly using Horn clauses and many recent advances in the Constraint/Logic Programming and Program Verification communities have centered around efficiently solving problems presented as Horn clauses. Since Horn clauses for verification and synthesis have been advocated by these communities in different times and from different perspectives, the HCVS workshop was organized to stimulate interaction and a fruitful exchange and integration of experiences.