Department of Information Technology

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.

Back to the seminar page

Updated  2012-11-05 13:47:42 by Frédéric Haziza.