Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Tue 15 Jan 2019 11:00 - 12:00 at Sala X - Session 4 Chair(s): Roberto Giacobazzi

Constrained Horn Clauses (CHCs) provide a suitable logical formalism for addressing a wide range of program verification problems. For this reason, a lot of effort has been recently devoted to the development of sophisticated solvers for checking the satisfiability of CHCs on various constraint theories (e.g., Linear Integer or Real Arithmetic, arrays, bitvectors, inductively defined data types). However, the effectiveness of solvers often depends on how the verification problem is encoded into clausal form, and suitable pre-processing techniques can significantly simplify the search for a satisfiability proof. In this talk we present recent and ongoing research on transformation techniques for CHCs that can be used to ease satisfiability proofs, and hence program verification. We follow a very general approach based on transformation rules such as unfolding, folding, and constraint rewriting. These rules are combined together in more complex transformation strategies, such as CHC specialization and predicate tupling. We demonstrate the usefulness of these transformations for various program verification tasks, such as proving partial correctness with respect to pre/post-conditions and proving relational properties (e.g., equivalence and non-interference). We also show that the approach based on CHC transformation is, to a large extent, language agnostic, by considering verification problems for programs written in various programming languages.

Making Proofs Easy: Horn Clause Transformations to the Aid of Program Verification (Invited Talk) (2019_Invited-PEPM.pdf)630KiB

Tue 15 Jan

pepm-2019-papers
11:00 - 12:30: PEPM 2019 - Session 4 at Sala X
Chair(s): Roberto GiacobazziUniversity of Verona and IMDEA Software Institute
pepm-2019-papers11:00 - 12:00
Talk
File Attached
pepm-2019-papers12:00 - 12:30
Talk
Kenny Zhuo Ming LuNanyang Polytechnic, Singapore
DOI