27 citations · 100 across the 15 of their papers we have counts for
15 papers
Catamorphic Abstractions for Constrained Horn Clause Satisfiability
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi +1
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 p…
Learning Brave Assumption-Based Argumentation Frameworks via ASP
Emanuele De Angelis, Maurizio Proietti, Francesca Toni
Assumption-based Argumentation (ABA) is advocated as a unifying formalism for various forms of non-monotonic reasoning, including logic programming. It allows capturing defeasible…
CHC-COMP 2023: Competition Report
Emanuele De Angelis, Hari Govind V K
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 Work…
ABA Learning via ASP
Emanuele De Angelis, Maurizio Proietti, Francesca Toni
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 neg…
CHC-COMP 2022: Competition Report
Emanuele De Angelis, Hari Govind V K
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…
Multiple Query Satisfiability of Constrained Horn Clauses
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi +1
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…
Verifying Catamorphism-Based Contracts using Constrained Horn Clauses
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi +1
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 (…
Satisfiability of Constrained Horn Clauses on Algebraic Data Types: A Transformation-based Approach
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi +1
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…
Solving Horn Clauses on Inductive Data Types Without Induction
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi +1
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 prop…
Predicate Pairing for Program Verification
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi +1
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). Ho…
Verification of Time-Aware Business Processes using Constrained Horn Clauses
Emanuele De Angelis, Fabio Fioravanti, Maria Chiara Meo +2
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.…
Removing Unnecessary Variables from Horn Clause Verification Conditions
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi +1
Verification conditions (VCs) are logical formulas whose satisfiability guarantees program correctness. We consider VCs in the form of constrained Horn clauses (CHC) which are auto…
Proving Correctness of Imperative Programs by Linearizing Constrained Horn Clauses
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi +1
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…
Verification of Programs by Combining Iterated Specialization with Interpolation
Emanuele De Angelis, Fabio Fioravanti, Jorge A. Navas +1
We present a verification technique for program safety that combines Iterated Specialization and Interpolating Horn Clause Solving. Our new method composes together these two techn…
Verification of Imperative Programs by Constraint Logic Program Transformation
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi +1
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 const…