413 citations
Counting papers with at most 25 authors, so collaboration author lists do not stand in for the people here.
- University of Rome Tor VergataIT38 papers
- Istituto di Analisi dei Sistemi ed Informatica Antonio RubertiIT19 papers
- Sapienza University of RomeIT18 papers
- University of PerugiaIT16 papers
- University of RostockDE11 papers
- National Research CouncilLK10 papers
- University of L'AquilaIT10 papers
- Centre National de la Recherche ScientifiqueFR9 papers
- Politecnico di MilanoIT9 papers
- The University of TokyoJP9 papers
- University of CagliariIT9 papers
- University of PaduaIT9 papers
20 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 (…
Universal Algebra in UniMath
Gianluca Amato, Matteo Calosci, Marco Maggesi +1
We present our library for Universal Algebra in the UniMath framework dealing with multi-sorted signatures, their algebras, and the basics for equation systems. We show how to impl…
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…
Universal Algebra in UniMath
Gianluca Amato, Marco Maggesi, Maurizio Parton +1
We present an ongoing effort to implement Universal Algebra in the UniMath system. Our aim is to develop a general framework for formalizing and studying Universal Algebra in a pro…
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…
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…
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…
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.…
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…
Proceedings First Workshop on Horn Clauses for Verification and Synthesis
Nikolaj Bjørner, Fabio Fioravanti, Andrey Rybalchenko +1
This volume contains the proceedings of HCVS 2014, the First Workshop on Horn Clauses for Verification and Synthesis which was held on July 17, 2014 in Vienna, Austria as a satelli…
Generalization Strategies for the Verification of Infinite State Systems
Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti +1
We present a method for the automated verification of temporal properties of infinite state systems. Our verification method is based on the specialization of constraint logic prog…
Decidability properties for fragments of CHR
Maurizio Gabbrielli abd Jacopo Mauro, Maria Chiara Meo, Jon Sneyers
We study the decidability of termination for two CHR dialects which, similarly to the Datalog like languages, are defined by using a signature which does not allow function symbols…
On the Expressive Power of Multiple Heads in CHR
Cinzia Di Giusto, Maurizio Gabbrielli, Maria Chiara Meo
Constraint Handling Rules (CHR) is a committed-choice declarative language which has been originally designed for writing constraint solvers and which is nowadays a general purpose…
Temporalized logics and automata for time granularity
M. Franceschet, A. Montanari
Suitable extensions of the monadic second-order theory of k successors have been proposed in the literature to capture the notion of time granularity. In this paper, we provide the…