Nagoya Termination Tool
Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe
TL;DR
The Nagoya Termination Tool is a new, efficient termination prover for term rewrite systems, featuring the first implementation of the weighted path order and strong integration with SMT solvers.
Contribution
It introduces the first implementation of the weighted path order and enhances efficiency through cooperation with external SMT solvers.
Findings
Successfully implements the weighted path order
Achieves high efficiency via SMT solver cooperation
Subsumes most existing reduction pairs
Abstract
This paper describes the implementation and techniques of the Nagoya Termination Tool, a termination prover for term rewrite systems. The main features of the tool are: the first implementation of the weighted path order which subsumes most of the existing reduction pairs, and the efficiency due to the strong cooperation with external SMT solvers. We present some new ideas that contribute to the efficiency and power of the tool.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Software Testing and Debugging Techniques