15 citations · 16 across the 4 of their papers we have counts for
4 papers
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…
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…