12 citations · 48 across the 17 of their papers we have counts for
Showing cs.LOShow all
3 papers · 1 filter
cs.LO2023
Choose your Colour: Tree Interpolation for Quantified Formulas in SMT
Elisabeth Henkel, Jochen Hoenicke, Tanja Schindler
We present a generic tree-interpolation algorithm in the SMT context with quantifiers. The algorithm takes a proof of unsatisfiability using resolution and quantifier instantiation…
cs.LO2019★ 1 cited
Interpolation and the Array Property Fragment
Jochen Hoenicke, Tanja Schindler
Interpolation based software model checkers have been successfully employed to automatically prove programs correct. Their power comes from interpolating SMT solvers that check the…
cs.LO2018
Efficient Interpolation for the Theory of Arrays
Jochen Hoenicke, Tanja Schindler
Existing techniques for Craig interpolation for the quantifier-free fragment of the theory of arrays are inefficient for computing sequence and tree interpolants: the solver needs…