de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch

Hilfe Wegweiser Datenschutzhinweis Impressum Kontakt

# Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Zeitschriftenartikel

#### Program termination analysis in polynomial time

##### MPG-Autoren
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44896

Lee,  Chin Soon
Programming Logics, MPI for Informatics, Max Planck Society;

##### Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
##### Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
##### Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
##### Zitation

Ben-Amram, A. M., & Lee, C. S. (2007). Program termination analysis in polynomial time. ACM Transactions on Programming Languages and Systems, 29(1), 5.1-5.37. doi:10.1145/1180475.1180480.

In an earlier work with Neil D.~Jones, we proposed the size-change principle'' for program termination: An infinite computation is \emph{impossible}, if it would imply that some data decrease in size infinitely. Such a property can be deduced from program analysis information in the form of \emph{size-change graphs}. A set of size-change graphs with the desired property is said to satisfy \emph{size-change termination} (SCT). There are many examples of practical programs whose termination can be verified by creating size-change graphs and testing them for SCT. While SCT is decidable, it has high worst-case complexity (complete for \sctext{pspace}). In this paper, we formulate an efficient approach to verify practical instances of SCT. Our procedure has worst-case complexity cubic in the input size. Its effectiveness is demonstrated empirically using a test-suite of over 90 programs.