Computing Interpolants without Proofs

Hana Chockler, Alexander Ivrii, Arie Matsliah

Research output: Chapter in Book/Report/Conference proceedingConference paperpeer-review

73 Downloads (Pure)

Abstract

We describe an incremental algorithm for computing interpolants for a pair ϕ A , ϕ B of formulas in propositional logic. In contrast with the common approaches, our method does not require a proof of unsatisfiability of ϕ A  ∧ ϕ B , and can be realized using any SAT solver as a black box. We achieve this by combining model enumeration with the ability to easily generate interpolants in the special case that one of the formulas is a cube.
Original languageEnglish
Title of host publicationHardware and Software: Verification and Testing - 8th International Haifa Verification Conference, HVC 2012. Revised Selected Papers
PublisherSpringer
Pages72-85
Number of pages14
Volume7857
Publication statusPublished - 6 Nov 2012

Publication series

NameLecture Notes in Computer Science
PublisherSpringer

Fingerprint

Dive into the research topics of 'Computing Interpolants without Proofs'. Together they form a unique fingerprint.

Cite this