Interpolation by Constraint Solving
Numerous symbolic model checking tools now use Craig interpolants when attempting to prove safety properties. Amongst the several known techniques for synthesizing interpolants, resolution based approaches are by far the most popular. Due to some open technical problem, an alternative approach based on constraint solving is not used in practice. Even the original pioneers of constraint-based interpolation methods now use resolution in their tools. In this talk, we present a solution facilitating the practical use of constraint-solving based approaches. Furthermore, our new technique gains a unique advantage which is shared by none of the existing methods.