Discovering Universally Quantified Solutions for Constrained Horn Clauses

Authors: Arie Gurfinkel, Sharon Shoham and Yakir Vizel

Paper Information

Title:Discovering Universally Quantified Solutions for Constrained Horn Clauses
Authors:Arie Gurfinkel, Sharon Shoham and Yakir Vizel
Proceedings:SMT Informal Proceedings
Editors: Rayna Dimitrova and Vijay D'Silva
Keywords:constrained horn clauses, inductive invariants, program verification, quantifier instantiation, quantifiers, property directed reachability, pdr, ic3

ABSTRACT. The logic of Constrained Horn Clauses (CHC) provides an effective logical characterization of many problems in (software) verification. For example, CHC naturally capture inductive invariant discovery for sequential programs, compositional verification of concurrent and distributed systems, and verification of program equivalence. CHC is used as an intermediate representation by several state-of-the-art program analysis tools, including SeaHorn and JayHorn.

Existing CHC solvers, such as Spacer and Eldarica, are limited to discovering quantifier free solutions. This severely limits their applicability in software verification where memory is modelled by arrays and quantifiers are necessary to express program properties. In this work, we extend the IC3 framework (used by Spacer CHC solver) to discover quantified solutions to CHC. Our work addresses two major challenges: (a) finding a sufficient set of instantiations that guarantees progress, and (b) finding and generalizing quantified candidate solutions. We have implemented our algorithm in Z3 and describe experiments with it in the context of software verification of C programs.

Talk:Jul 13 14:00 (Session 87K)