Electronic Proceedings in Theoretical Computer Science (Jul 2019)

Ultimate TreeAutomizer (CHC-COMP Tool Description)

  • Daniel Dietsch,
  • Matthias Heizmann,
  • Jochen Hoenicke,
  • Alexander Nutz,
  • Andreas Podelski

DOI
https://doi.org/10.4204/EPTCS.296.7
Journal volume & issue
Vol. 296, no. Proc. HCVS/PERR 2019
pp. 42 – 47

Abstract

Read online

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 attractive properties in terms of expressiveness and accessibility to algorithmic solving. Ultimate TreeAutomizer is based on the techniques of trace abstraction, tree automata and tree interpolation. This paper serves as a tool description for TreeAutomizer in CHC-COMP 2019.