27 citations · 101 across the 19 of their papers we have counts for
19 papers
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…
Transformational Verification of Quicksort
Emanuele De Angelis, Fabio Fioravanti, Maurizio Proietti
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 ve…
Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi +1
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 tr…
Lemma Generation for Horn Clause Satisfiability: A Preliminary Study
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi +1
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 che…