Interpolation by Constraint Solving
Hongyi Chen ( Louisiana State University )
- 11:30 8th March 2013 ( week 8, Hilary Term 2013 )278
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:
