2 citations · 3 across the 4 of their papers we have counts for
6 papers · 1 filter
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…
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…
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…
Proving Properties of Sorting Programs: A Case Study in Horn Clause Verification
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi +1
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…
Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning
Emanuele De Angelis, Grigory Fedyukovich, Nikos Tzevelekos +1
This volume contains the joint post-proceedings of the 3rd Workshop on Program Equivalence and Relational Reasoning (PERR) and the 6th Workshop on Horn Clauses for Verification and…
Enhancing Predicate Pairing with Abstraction for Relational Verification
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi +1
Relational verification is a technique that aims at proving properties that relate two different program fragments, or two different program runs. It has been shown that constraine…