Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Automated Termination Proofs for Java Bytecode with Cyclic Data

Marc Brockschmidt, Richard Musiol, Carsten Otto, and Juergen Giesl

Abstract

In earlier work, we developed a technique to prove termination of Java programs automatically: first, Java programs are automatically transformed to term rewrite systems (TRSs) and then, existing methods and tools are used to prove termination of the resulting TRSs. In this paper, we extend our technique in order to prove termination of algorithms on cyclic data such as cyclic lists or graphs automatically. We implemented our technique in the tool AProVE and performed extensive experiments to evaluate its practical applicability.

Details

Publication typeInproceedings
Published inCAV
> Publications > Automated Termination Proofs for Java Bytecode with Cyclic Data