15 citations · 17 across the 4 of their papers we have counts for
4 papers
Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification
Petra Hozzová, Jaroslav Bendík, Alexander Nutz +1
The need to solve non-linear arithmetic constraints presents a major obstacle to the automatic verification of smart contracts. In this case study we focus on the two overapproxima…
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…
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…