# Ultimate TreeAutomizer (CHC-COMP Tool Description)

**Authors:** 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)

arXiv: 1907.03998 · 2019-07-10

## TL;DR

Ultimate TreeAutomizer is a solver for satisfiability of constrained Horn clauses, utilizing trace abstraction, tree automata, and interpolation, presented as a tool for CHC-COMP 2019.

## Contribution

It introduces Ultimate TreeAutomizer, a novel solver combining trace abstraction, tree automata, and interpolation for CHC satisfiability.

## Key findings

- Successfully participated in CHC-COMP 2019.
- Demonstrates effectiveness of combined techniques.
- Provides a detailed tool description for the community.

## Abstract

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.

## Full text

_Full body text omitted from this summary view._ Fetch the complete paper as Markdown: https://tomesphere.com/paper/1907.03998/full.md

## Figures

2 figures with captions in the complete paper: https://tomesphere.com/paper/1907.03998/full.md

## References

20 references — full list in the complete paper: https://tomesphere.com/paper/1907.03998/full.md

---
Source: https://tomesphere.com/paper/1907.03998