*Result*: Automated termination proofs for Java programs with cyclic data
Title:
Automated termination proofs for Java programs with cyclic data
Authors:
Contributors:
The Pennsylvania State University CiteSeerX Archives
Publication Year:
2012
Collection:
CiteSeerX
Document Type:
*Academic Journal*
text
File Description:
application/pdf
Language:
English
Availability:
Rights:
Metadata may be used without restrictions as long as the oai identifier remains attached to it.
Accession Number:
edsbas.4D2D89A6
Database:
BASE
*Further Information*
*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. 1*