Ultimate TreeAutomizer (CHC-COMP Tool Description)

Daniel Dietsch
(University of Freiburg) 		Matthias Heizmann
(University of Freiburg) 		Jochen Hoenicke
(University of Freiburg) 		Alexander Nutz
(University of Freiburg) 		Andreas Podelski
(University of Freiburg)

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.

In Emanuele De Angelis, Grigory Fedyukovich, Nikos Tzevelekos and Mattias Ulbrich: Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning (HCVS/PERR 2019), Prague, Czech Republic, 6-7th April 2019, Electronic Proceedings in Theoretical Computer Science 296, pp. 42–47.
Published: 9th July 2019.
ArXived at: https://dx.doi.org/10.4204/EPTCS.296.7 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org