3 citations · 3 across the 3 of their papers we have counts for
3 papers
cs.LO2017
Proof Tree Preserving Interpolation
Jürgen Christ, Jochen Hoenicke, Alexander Nutz
Craig interpolation in SMT is difficult because, e. g., theory combination and integer cuts introduce mixed literals, i. e., literals containing local symbols from both input formu…
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…