15 citations · 19 across the 10 of their papers we have counts for
3 papers · 1 filter
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…