3 citations · 3 across the 3 of their papers we have counts for
3 papers
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.LO2014
Weakly Equivalent Arrays
Jürgen Christ, Jochen Hoenicke
The (extensional) theory of arrays is widely used to model systems. Hence, efficient decision procedures are needed to model check such systems. Current decision procedures for the…
cs.PL2012★ 3 cited
Towards Bounded Infeasible Code Detection
Jürgen Christ, Jochen Hoenicke, Martin Schäf
A first step towards more reliable software is to execute each statement and each control-flow path in a method once. In this paper, we present a formal method to automatically com…