27 citations · 101 across the 22 of their papers we have counts for
15 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…
Contract Strengthening through Constrained Horn Clause Verification
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi +1
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 prec…
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 (…
Analysis and Transformation of Constrained Horn Clauses for Program Verification
Emanuele De Angelis, Fabio Fioravanti, John P. Gallagher +3
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 soft…
A Historical Account of My Early Research Interests
Alberto Pettorossi
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 Comput…