A Proof-Sensitive Approach for Small Propositional Interpolants
VSTTE, pp. 1-18, 2015.
The labeled interpolation system LIS is a framework for Craig interpolation widely used in propositional-satisfiability-based model checking. Most LIS-based algorithms construct the interpolant from a proof of unsatisfiability and a fixed labeling determined by which part of the propositional formula is being over-approximated. While this...More
Full Text (Upload PDF)
PPT (Upload PPT)