Searcharxiv⌕ Search

arXiv subjects

Emanuele De Angelis

Publications and source records attributed to Emanuele De Angelis.

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↗
arXiv2025

Object-Centric Neuro-Argumentative Learning

Over the last decade, as we rely more on deep learning technologies to make critical decisions, concerns regarding their safety, reliability and interpretability have emerged. We introduce a novel Neural Argumentative Learning (NAL) architecture that integrates Assumption-Based Argumentation (ABA) with deep learning for image analysis. Our architecture consists of neural and symbolic components. The former segments and encodes images into facts using object-centric learning, while the latter applies ABA learning to develop ABA frameworks enabling predictions with images. Experiments on synthetic data show that the NAL architecture can be competitive with a state-of-the-art alternative.

cs.LG↗
arXiv2024

Learning Brave Assumption-Based Argumentation Frameworks via ASP

Assumption-based Argumentation (ABA) is advocated as a unifying formalism for various forms of non-monotonic reasoning, including logic programming. It allows capturing defeasible knowledge, subject to argumentative debate. While, in much existing work, ABA frameworks are given up-front, in this paper we focus on the problem of automating their learning from background knowledge and positive/negative examples. Unlike prior work, we newly frame the problem in terms of brave reasoning under stable extensions for ABA. We present a novel algorithm based on transformation rules (such as Rote Learning, Folding, Assumption Introduction and Fact Subsumption) and an implementation thereof that makes use of Answer Set Programming. Finally, we compare our technique to state-of-the-art ILP systems that learn defeasible knowledge.

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

CHC-COMP 2023: Competition Report

CHC-COMP 2023 is the sixth edition of the Competition of Solvers for Constrained Horn Clauses. The competition was run in April 2023 and the results were presented at the 10th Workshop on Horn Clauses for Verification and Synthesis held in Paris, France, on April 23, 2023. This edition featured seven solvers (six competing and one hors concours) and six tracks, each of which dealing with a class of clauses. This report describes the organization of CHC-COMP 2023 and presents its results.

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↗
arXiv2023

ABA Learning via ASP

Recently, ABA Learning has been proposed as a form of symbolic machine learning for drawing Assumption-Based Argumentation frameworks from background knowledge and positive and negative examples. We propose a novel method for implementing ABA Learning using Answer Set Programming as a way to help guide Rote Learning and generalisation in ABA Learning.

cs.AI↗
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

CHC-COMP 2022: Competition Report

CHC-COMP 2022 is the fifth edition of the competition of solvers for Constrained Horn Clauses. The competition was run in March 2022; the results were presented at the 9th Workshop on Horn Clauses for Verification and Synthesis held in Munich, Germany, on April 3, 2022. This edition featured six solvers, and eight tracks consisting of sets of linear and nonlinear clauses with constraints over linear integer arithmetic, linear real arithmetic, arrays, and algebraic data types. This report provides an overview of the organization behind the competition runs: it includes the technical details of the competition setup as well as presenting the results of the 2022 edition.

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

Pre-proceedings of the 31st International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2021)

This volume constitutes the pre-proceedings of the 31st International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2021), held on 7-8th September 2021 as a hybrid (blended) meeting, both in-person (at the Teachers' House in Tallinn, Estonia) and virtual, and co-located with the 23rd International Symposium on Principles and Practice of Declarative Programming (PPDP 2021). After discussion at the symposium papers will go through a second round of refereeing and selection for the formal proceedings.

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

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.

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↗