Ultimate TreeAutomizer (CHC-COMP Tool Description).
European Joint Conferences on Theory And Practice of Software(2019)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络