15 citations · 22 across the 5 of their papers we have counts for
5 papers
Proving LTL Properties of Bitvector Programs and Decompiled Binaries (Extended)
Yuandong Cyrus Liu, Chengbin Pang, Daniel Dietsch +4
There is increasing interest in applying verification tools to programs that have bitvector operations (eg., binaries). SMT solvers, which serve as a foundation for these tools, ha…
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…
Refining Trace Abstraction using Abstract Interpretation
Marius Greitschus, Daniel Dietsch, Andreas Podelski
The CEGAR loop in software model checking notoriously diverges when the abstraction refinement procedure does not derive a loop invariant. An abstraction refinement procedure based…
Monitoring Student Activity in Collaborative Software Development
Daniel Dietsch, Andreas Podelski, Jaechang Nam +2
This paper presents data analysis from a course on Software Engineering in an effort to identify metrics and techniques that would allow instructor to act proactively and identify…