15 citations · 19 across the 10 of their papers we have counts for
11 papers
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…
Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems
Oded Padon, Jochen Hoenicke, Kenneth L. McMillan +3
Various verification techniques for temporal properties transform temporal verification to safety verification. For infinite-state systems, these transformations are inherently imp…
Ultimate TreeAutomizer (CHC-COMP Tool Description)
Daniel Dietsch, Matthias Heizmann, Jochen Hoenicke +2
We present Ultimate TreeAutomizer, a solver for satisfiability of sets of constrained Horn clauses. Constrained Horn clauses (CHC) are a fragment of first order logic with attracti…
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…
Different Maps for Different Uses. A Program Transformation for Intermediate Verification Languages
Daniel Dietsch, Matthias Heizmann, Jochen Hoenicke +2
In theorem prover or SMT solver based verification, the program to be verified is often given in an intermediate verification language such as Boogie, Why, or CHC. This setting rai…
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…