Researcher profile

Emanuele De Angelis

Emanuele De Angelis contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate

Logic in Computer Science Programming Languages Software Engineering

Trust snapshot

Quick read

Trust 21 - Emerging

7works

0followers

3topics

4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

preprint2022arXiv

Verifying Catamorphism-Based Contracts using Constrained Horn Clauses

We address the problem of verifying that the functions of a program meet their contracts, specified by pre/postconditions. We follow an approach based on constrained Horn clauses (CHCs) by which the verification problem is reduced to the problem of checking satisfiability of a set of clauses derived from the given program and contracts. We consider programs that manipulate algebraic data types (ADTs) and a class of contracts specified by catamorphisms, that is, functions defined by simple recursion schemata on the given ADTs. We show by several examples that state-of-the-art CHC satisfiability tools are not effective at solving the satisfiability problems obtained by direct translation of the contracts into CHCs. To overcome this difficulty, we propose a transformation technique that removes the ADT terms from CHCs and derives new sets of clauses that work on basic sorts only, such as integers and booleans. Thus, when using the derived CHCs there is no need for induction rules on ADTs. We prove that the transformation is sound, that is, if the derived set of CHCs is satisfiable, then so is the original set. We also prove that the transformation always terminates for the class of contracts specified by catamorphisms. Finally, we present the experimental results obtained by an implementation of our technique when verifying many non-trivial contracts for ADT manipulating programs.

preprint2020arXiv

Transformational Verification of Quicksort

Many transformation techniques developed for constraint logic programs, also known as constrained Horn clauses (CHCs), have found new useful applications in the field of program verification. In this paper, we work out a nontrivial case study through the transformation-based verification approach. We consider the familiar Quicksort program for sorting lists, written in a functional programming language, and we verify the pre/-postconditions that specify the intended correctness properties of the functions defined in the program. We verify these properties by: (1) translating them into CHCs, (2) transforming the CHCs by removing all list occurrences, and (3) checking the satisfiability of the transformed CHCs by using the Eldarica solver over booleans and integers. The transformation mentioned at Point (2) requires an extension of the algorithms for the elimination of inductively defined data structures presented in previous work, because during one stage of the transformation we use as lemmas some properties that have been proved at previous stages.

preprint2016arXiv

Removing Unnecessary Variables from Horn Clause Verification Conditions

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.

preprint2016arXiv

Verification of Time-Aware Business Processes using Constrained Horn Clauses

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.

preprint2015arXiv

Proving Correctness of Imperative Programs by Linearizing Constrained Horn Clauses

We present a method for verifying the correctness of imperative programs which is based on the automated transformation of their specifications. Given a program prog, we consider a partial correctness specification of the form $\{φ\}$ prog $\{ψ\}$, where the assertions $φ$ and $ψ$ are predicates defined by a set Spec of possibly recursive Horn clauses with linear arithmetic (LA) constraints in their premise (also called constrained Horn clauses). The verification method consists in constructing a set PC of constrained Horn clauses whose satisfiability implies that $\{φ\}$ prog $\{ψ\}$ is valid. We highlight some limitations of state-of-the-art constrained Horn clause solving methods, here called LA-solving methods, which prove the satisfiability of the clauses by looking for linear arithmetic interpretations of the predicates. In particular, we prove that there exist some specifications that cannot be proved valid by any of those LA-solving methods. These specifications require the proof of satisfiability of a set PC of constrained Horn clauses that contain nonlinear clauses (that is, clauses with more than one atom in their premise). Then, we present a transformation, called linearization, that converts PC into a set of linear clauses (that is, clauses with at most one atom in their premise). We show that several specifications that could not be proved valid by LA-solving methods, can be proved valid after linearization. We also present a strategy for performing linearization in an automatic way and we report on some experimental results obtained by using a preliminary implementation of our method.

preprint2014arXiv

Verification of Programs by Combining Iterated Specialization with Interpolation

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.

preprint2013arXiv

Verification of Imperative Programs by Constraint Logic Program Transformation

We present a method for verifying partial correctness properties of imperative programs that manipulate integers and arrays by using techniques based on the transformation of constraint logic programs (CLP). We use CLP as a metalanguage for representing imperative programs, their executions, and their properties. First, we encode the correctness of an imperative program, say prog, as the negation of a predicate 'incorrect' defined by a CLP program T. By construction, 'incorrect' holds in the least model of T if and only if the execution of prog from an initial configuration eventually halts in an error configuration. Then, we apply to program T a sequence of transformations that preserve its least model semantics. These transformations are based on well-known transformation rules, such as unfolding and folding, guided by suitable transformation strategies, such as specialization and generalization. The objective of the transformations is to derive a new CLP program TransfT where the predicate 'incorrect' is defined either by (i) the fact 'incorrect.' (and in this case prog is not correct), or by (ii) the empty set of clauses (and in this case prog is correct). In the case where we derive a CLP program such that neither (i) nor (ii) holds, we iterate the transformation. Since the problem is undecidable, this process may not terminate. We show through examples that our method can be applied in a rather systematic way, and is amenable to automation by transferring to the field of program verification many techniques developed in the field of program transformation.