Automatic termination analysis for functional and imperative programs (Thesis, TU Darmstadt) (Q2726244)

Verifying the termination of algorithms is a central problem in computer science. The authors present a new method for automating termination proofs for functional and imperative programs.NEWLINENEWLINENEWLINEIn authors' approach, an imperative program is translated into an equivalent functional one whose termination is analyzed instead. In general, this translation yields recursive sub-procedures which terminate only partially, i.e., if their inputs satisfy certain preconditions. However, previous methods for functional programs try to prove that each procedure terminates totally, i.e., for each input.NEWLINENEWLINENEWLINEThe authors present the approach to analyzing the terminating behavior of partially terminating procedures by machine. Their proposal generalizes earlier works and provides a method for proving termination of several functional and imperative programs without human interaction.NEWLINENEWLINENEWLINEThe book has the following structure. Chapter 1 is the introduction to the book. Chapter 2 introduces the employed functional programming languge and the logic to express statements about functional procedures. In Chapter 3, the authors give a survey of Giesl's approach to generating polynomial norms and enrich it with new techniques. In Chapter 7 a general method for the synthesis of termination predicate procedures is presented. The techniques for the generation of polynomial norms presented in Chapter 3 are generalized for termination predicate synthesis in Chapter 5. In Chapter 6, the authors present some techniques to automatically simplify the procedures synthesized by their method. In Chapter 7 a solution for induction theorem proving for partial functions with termination predicates is presented. In Chapter 8, the authors extend their programming language with imperative statements and apply their method to imperative programs. In Chapter 9, they evaluate their approach comparing it to related works, showing its strengths and limitations and drawing some conclusions. In Appendix A, they summarize some heuristics, borrowed from Giesl's work to optimize their approach. Appendix B contains a collection of functional and imperative procedures.