
Analysis and Transformation of Constrained Horn Clauses for Program Verification
This paper surveys recent work on applying analysis and transformation t...
read it

Preproceedings of the 31st International Symposium on LogicBased Program Synthesis and Transformation (LOPSTR 2021)
This volume constitutes the preproceedings of the 31st International Sy...
read it

Transformational Verification of Quicksort
Many transformation techniques developed for constraint logic programs, ...
read it

Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates
We address the problem of proving the satisfiability of Constrained Horn...
read it

Lemma Generation for Horn Clause Satisfiability: A Preliminary Study
It is known that the verification of imperative, functional, and logic p...
read it

Proving Properties of Sorting Programs: A Case Study in Horn Clause Verification
The proof of a program property can be reduced to the proof of satisfiab...
read it

Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning
This volume contains the joint postproceedings of the 3rd Workshop on P...
read it

Bounded Symbolic Execution for Runtime Error Detection of Erlang Programs
Dynamically typed languages, like Erlang, allow developers to quickly wr...
read it

Solving Horn Clauses on Inductive Data Types Without Induction
We address the problem of verifying the satisfiability of Constrained Ho...
read it

Enhancing Predicate Pairing with Abstraction for Relational Verification
Relational verification is a technique that aims at proving properties t...
read it

Predicate Pairing for Program Verification
It is wellknown that the verification of partial correctness properties...
read it
Emanuele De Angelis
is this you? claim profile