Skip to main content

Interpolation by Constraint Solving

Hongyi Chen ( Louisiana State University )

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.

Speaker bio

Hongyi Chen is a PhD in the Department of Computer Science at Louisiana State University. She is passionate about program analysis, model checking, and automated deduction. Specifically she has been working on the topics such as reachability analysis, termination analysis, and bound synthesis.

Share this: