Proving Termination of Programs Automatically with AProVE

Authors: Jürgen Giesl, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Stroeder, Steffi Swiderski and Rene Thiemann

Title:	Proving Termination of Programs Automatically with AProVE
Authors:	Jürgen Giesl, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Stroeder, Steffi Swiderski and Rene Thiemann
Proceedings:	IJCAR 2014 LNCS proceedings
Editors:	Stéphane Demri, Deepak Kapur and Christoph Weidenbach
Keywords:	termination, complexity, program analysis, Java, Haskell, Prolog, term rewriting
Abstract:	ABSTRACT. AProVE is a system for automated termination and complexity proofs of Java, Haskell, Prolog, and term rewrite systems (TRSs). To analyze programs in high-level programming languages, AProVE automatically converts them to TRSs. Then, a wide range of techniques is employed to prove termination and to infer complexity bounds for the resulting TRSs. Finally, the generated proofs can be exported to certify their correctness using automatic theorem proving techniques. For use in software construction, we present an AProVE plug-in for the popular Eclipse software development environment.
Pages:	7
Talk:	Jul 20 12:15
Paper: