Termination tools: Verification and Optimization

The aim of this project is to make tools that automatically prove termination of term rewrite systems 1. more reliable by certifying termination techniques that are used in these tools in the Isabelle/HOL proof assistant, 2. more efficient by applying BDD technology to obtain compact representations of the large search spaces that go hand in hand with powerful termination techniques, 3. more useful by permitting rewriting formats that model higher-order aspects as found in functional programming and theorem proving systems. A further aim is 4. to use recent termination techniques employed in termination tools to increase the usability of Isabelle/HOL by enlarging the class of recursive functions that it accepts without requiring a user-supplied termination proof. The termination technique that we focus on in items 1 and 4 is the variant of the dependency pair method based on the recent subterm criterion of Hirokawa and Middeldorp. The initial focus in item 2 is on the basic version of the dependency pair method in which argument filterings are used in connection with a strongly monotone base order like the lexicographic path order. Finally, a new uncurrying transformation will form the basis for item 3. The techniques developed in items 2 and 3 will be incorporated in the Tyrolean Termination Tool.

Proving the correctness of computer software is of utmost importance for safety-critical systems (like fire alarms, fly-by-wire systems, human spaceflight, nuclear reactors, robotic surgery, etc.). A crucial part of proving correctness is to show that a computer program yields a result, as it may run forever otherwise. This property is called termination and is undecidable in general. However, there are so called termination tools which are able to prove termination automatically in surprisingly many cases. In this project we increased the power of termination tools by developing new techniques of proving termination as well as improving some of the existing techniques. It turned out to be beneficial if termination techniques are not implemented by dedicated algorithms. Instead, they are transformed into a different problem domain (SMT) and uniformly solved by specialized tools. This approach allows to implement traditional criteria with less effort and typically the overall runtime is also reduced. Since termination tools themselves are just computer programs, they may contain bugs and thus produce wrong results (this actually happened already a few times). Therefore, the current trend is to automatically certify termination proofs that were generated by a termination tool, using a theorem prover. This requires that all the termination techniques that are used in such a proof, are proved correct with the theorem prover, which is much more involved than proving facts on paper, since we need to be able to break down every proof into atomic steps that can be understood by the theorem prover. As a result the proof in the theorem prover is very unlikely to contain erroneous deduction steps. In this project, we carried out such correctness proofs for many techniques that are used by some termination tool; enabling us to certify numerous proofs that are generated by state-of-the-art termination tools.