arXiv subjects

Alberto Pettorossi

Publications and source records attributed to Alberto Pettorossi.

At least 19 recordsLinked to original sources

arXiv2026

Constrained Assumption-Based Argumentation Frameworks

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.

cs.AI↗

arXiv2024

Catamorphic Abstractions for Constrained Horn Clause Satisfiability

Catamorphisms are functions that are recursively defined on list and trees and, in general, on Algebraic Data Types (ADTs), and are often used to compute suitable abstractions of programs that manipulate ADTs. Examples of catamorphisms include functions that compute size of lists, orderedness of lists, and height of trees. It is well known that program properties specified through catamorphisms can be proved by showing the satisfiability of suitable sets of Constrained Horn Clauses (CHCs). We address the problem of checking the satisfiability of those sets of CHCs, and we propose a method for transforming sets of CHCs into equisatisfiable sets where catamorphisms are no longer present. As a consequence, clauses with catamorphisms can be handled without extending the satisfiability algorithms used by existing CHC solvers. Through an experimental evaluation on a non-trivial benchmark consisting of many list and tree processing algorithms expressed as sets of CHCs, we show that our technique is indeed effective and significantly enhances the performance of state-of-the-art CHC solvers.

cs.LO↗

arXiv2024

Multiple Query Satisfiability of Constrained Horn Clauses

We address the problem of checking the satisfiability of a set of constrained Horn clauses (CHCs) possibly including more than one query. We propose a transformation technique that takes as input a set of CHCs, including a set of queries, and returns as output a new set of CHCs, such that the transformed CHCs are satisfiable if and only if so are the original ones, and the transformed CHCs incorporate in each new query suitable information coming from the other ones so that the CHC satisfiability algorithm is able to exploit the relationships among all queries. We show that our proposed technique is effective on a non trivial benchmark of sets of CHCs that encode many verification problems for programs manipulating algebraic data types such as lists and trees.

cs.LO↗

arXiv2022

Contract Strengthening through Constrained Horn Clause Verification

The functional properties of a program are often specified by providing a contract for each of its functions. A contract of a function consists of a pair of formulas, called a precondition and a postcondition, which, respectively, should hold before and after execution of that function. It might be the case that the contracts supplied by the programmer are not adequate to allow a verification system to prove program correctness, that is, to show that for every function, if the precondition holds and the execution of the function terminates, then the postcondition holds. We address this problem by providing a technique which may strengthen the postconditions of the functions, thereby improving the ability of the verifier to show program correctness. Our technique consists of four steps. First, the translation of the given program, which may manipulate algebraic data structures (ADTs), and its contracts into a set of constrained Horn clauses (CHCs) whose satisfiability implies the validity of the given contracts. Then, the derivation, via CHC transformation performed by the VeriCaT tool, of a new set of CHCs that manipulate only basic sorts (such as booleans or integers) and whose satisfiability implies the satisfiability of the original set of clauses. Then, the construction of a model, if any, of the new, derived CHCs using the CHC solver SPACER for basic sorts. Finally, the translation of that model into the formulas that suitably strengthen the postconditions of the given contracts. We will present our technique through an example consisting of a Scala program for reversing lists. Note that the Stainless verifier is not able to prove the correctness of that program when considering the given contracts, while it succeeds when considering the contracts with the strengthened postconditions constructed by applying our technique.

cs.LO↗

arXiv2022

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.

cs.LO↗

arXiv2021

Satisfiability of Constrained Horn Clauses on Algebraic Data Types: A Transformation-based Approach

We address the problem of checking the satisfiability of Constrained Horn Clauses (CHCs) defined on Algebraic Data Types (ADTs), such as lists and trees. We propose a new technique for transforming CHCs defined on ADTs into CHCs where the arguments of the predicates have only basic types, such as integers and booleans. Thus, our technique avoids, during satisfiability checking, the explicit use of proof rules based on induction over the ADTs. The main extension over previous techniques for ADT removal is a new transformation rule, called differential replacement, which allows us to introduce auxiliary predicates, whose definitions correspond to lemmas that are used when making inductive proofs. We present an algorithm that performs the automatic removal of ADTs by applying the new rule, together with the traditional folding/unfolding rules. We prove that, under suitable hypotheses, the set of the transformed clauses is satisfiable if and only if so is the set of the original clauses. By an experimental evaluation, we show that the use of the new rule significantly improves the effectiveness of ADT removal. We also show that our approach is competitive with respect to tools that extend CHC solvers with the use of inductive rules.

cs.PL↗

arXiv2021

Analysis and Transformation of Constrained Horn Clauses for Program Verification

This paper surveys recent work on applying analysis and transformation techniques that originate in the field of constraint logic programming (CLP) to the problem of verifying software systems. We present specialisation-based techniques for translating verification problems for different programming languages, and in general software systems, into satisfiability problems for constrained Horn clauses (CHCs), a term that has become popular in the verification field to refer to CLP programs. Then, we describe static analysis techniques for CHCs that may be used for inferring relevant program properties, such as loop invariants. We also give an overview of some transformation techniques based on specialisation and fold/unfold rules, which are useful for improving the effectiveness of CHC satisfiability tools. Finally, we discuss future developments in applying these techniques.

cs.LO↗

arXiv2020

Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates

We address the problem of proving the satisfiability of Constrained Horn Clauses (CHCs) with Algebraic Data Types (ADTs), such as lists and trees. We propose a new technique for transforming CHCs with ADTs into CHCs where predicates are defined over basic types, such as integers and booleans, only. Thus, our technique avoids the explicit use of inductive proof rules during satisfiability proofs. The main extension over previous techniques for ADT removal is a new transformation rule, called differential replacement, which allows us to introduce auxiliary predicates corresponding to the lemmas that are often needed when making inductive proofs. We present an algorithm that uses the new rule, together with the traditional folding/unfolding transformation rules, for the automatic removal of ADTs. We prove that if the set of the transformed clauses is satisfiable, then so is the set of the original clauses. By an experimental evaluation, we show that the use of the differential replacement rule significantly improves the effectiveness of ADT removal, and we show that our transformation-based approach is competitive with respect to a well-established technique that extends the CVC4 solver with induction.

cs.PL↗

arXiv2020

A Historical Account of My Early Research Interests

This paper presents a brief account of some of the my early research interests. This historical account starts from my laurea thesis on Signal Theory and my master thesis on Computation Theory. It recalls some results in Combinatory Logic and Term Rewriting Systems. Some other results concern Program Transformation, Parallel Computation, Theory of Concurrency, and Proof of Program Properties. My early research activity has been mainly done in cooperation with Andrzej Skowron, Anna Labella, and Maurizio Proietti.

cs.LO↗

arXiv2019

Lemma Generation for Horn Clause Satisfiability: A Preliminary Study

It is known that the verification of imperative, functional, and logic programs can be reduced to the satisfiability of constrained Horn clauses (CHCs), and this satisfiability check can be performed by using CHC solvers, such as Eldarica and Z3. These solvers perform well when they act on simple constraint theories, such as Linear Integer Arithmetic and the theory of Booleans, but their efficacy is very much reduced when the clauses refer to constraints on inductively defined structures, such as lists or trees. Recently, we have presented a transformation technique for eliminating those inductively defined data structures, and hence avoiding the need for incorporating induction principles into CHC solvers. However, this technique may fail when the transformation requires the use of lemmata whose generation needs ingenuity. In this paper we show, through an example, how during the process of transforming CHCs for eliminating inductively defined structures one can introduce suitable predicates, called difference predicates, whose definitions correspond to the lemmata to be introduced. Through a second example, we show that, whenever difference predicates cannot be introduced, we can introduce, instead, auxiliary queries which also correspond to lemmata, and the proof of these lemmata can be done by showing the satisfiability of those queries.

cs.LO↗

arXiv2019

Proving Properties of Sorting Programs: A Case Study in Horn Clause Verification

The proof of a program property can be reduced to the proof of satisfiability of a set of constrained Horn clauses (CHCs) which can be automatically generated from the program and the property. In this paper we have conducted a case study in Horn clause verification by considering several sorting programs with the aim of exploring the effectiveness of a transformation technique which allows us to eliminate inductive data structures such as lists or trees. If this technique is successful, we derive a set of CHCs with constraints over the integers and booleans only, and the satisfiability check can often be performed in an effective way by using state-of-the-art CHC solvers, such as Eldarica or Z3. In this case study we have also illustrated the usefulness of a companion technique based on the introduction of the so-called difference predicates, whose definitions correspond to lemmata required during the verification. We have considered functional programs which implement the following kinds of sorting algorithms acting on lists of integers: (i) linearly recursive sorting algorithms, such as insertion sort and selection sort, and (ii) non-linearly recursive sorting algorithms, such as quicksort and mergesort, and we have considered the following properties: (i) the partial correctness properties, that is, the orderedness of the output lists, and the equality of the input and output lists when viewed as multisets, and (ii) some arithmetic properties, such as the equality of the sum of the elements before and after sorting.

cs.LO↗

arXiv2018

Bounded Symbolic Execution for Runtime Error Detection of Erlang Programs

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 those languages less reliable than statically typed languages, where many runtime errors can be detected at compile time. In this paper, we present a 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 for that program, returns answer constraints that represent sets of concrete data for which the Erlang program generates a runtime error.

cs.PL↗

arXiv2018

Regularity of languages generated by non context-free grammars over a singleton terminal alphabet

It is well-known that: (i) every context-free language over a singleton terminal alphabet is regular, and (ii) the class of languages that satisfy the Pumping Lemma is a proper super-class of the context-free languages. We show that any language in this superclass over a singleton terminal alphabet is regular. Our proof is based on a transformational approach and does not rely on Parikh's Theorem. Our result extends previously known results because there are languages that are not context-free, do satisfy the Pumping Lemma, and do not satisfy the hypotheses of Parikh's Theorem.

cs.FL↗

arXiv2018

Predicate Pairing for Program Verification

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.

cs.LO↗

arXiv2018

Solving Horn Clauses on Inductive Data Types Without Induction

We address the problem of verifying the satisfiability of Constrained Horn Clauses (CHCs) based on theories of inductively defined data structures, such as lists and trees. We propose a transformation technique whose objective is the removal of these data structures from CHCs, hence reducing their satisfiability to a satisfiability problem for CHCs on integers and booleans. We propose a transformation algorithm and identify a class of clauses where it always succeeds. We also consider an extension of that algorithm, which combines clause transformation with reasoning on integer constraints. Via an experimental evaluation we show that our technique greatly improves the effectiveness of applying the Z3 solver to CHCs. We also show that our verification technique based on CHC transformation followed by CHC solving, is competitive with respect to CHC solvers extended with induction. This paper is under consideration for acceptance in TPLP.

cs.LO↗

arXiv2017

Enhancing Predicate Pairing with Abstraction for Relational Verification

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.

cs.LO↗

arXiv2016

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.

cs.LO↗

arXiv2016

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.

cs.LO↗