Interpolation and Horn Clauses
Speaker
Hossein Hojjat
, EPFL Lausanne
Date and Time
Wednesday, November 7th, 2012 at 10:30
Location
Polacksbacken, room 2247
Abstract
The problem of program verification reduces to finding the solution to a set of recursive Horn clauses. An effective way for solving recursive Horn clauses is the interpolation-based predicate abstraction technique. This approach verifies a conservative abstraction of the Horn clauses with respect to a set of predicates. If the abstraction does not lead to an error or discloses a real bug in the original clauses the procedure terminates. Otherwise the system further refines the abstraction by solving the spurious counter-example in form of finite recursion-free set of Horn clauses.
In this talk we identify the correspondence between solving different fragments of recursion-free Horn clauses with different notions of interpolation such as interpolation-sequence or tree-interpolation. We then introduce the notion of disjunctive interpolation and show that the solution to a set of recursion-free Horn clauses in general is essentially equivalent to computing disjunctive interpolants. We give certain complexity bounds for solving recursion-free Horn clauses in propositional logic and Presburger arithmetic.