27 citations · 100 across the 15 of their papers we have counts for
11 papers · 1 filter
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…
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…
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 (…
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…