A region graph based approach to termination proofs


Dateien zu dieser Ressource

Prüfsumme: MD5:f4c7d72f50d0bcf770dec6c49d7be460

LEUE, Stefan, Wei WEI, 2006. A region graph based approach to termination proofs. In: HERMANNS, Holger, ed., Jens PALSBERG, ed.. Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg:Springer Berlin Heidelberg, pp. 318-333. ISBN 978-3-540-33056-1

@inproceedings{Leue2006regio-21457, title={A region graph based approach to termination proofs}, year={2006}, doi={10.1007/11691372_21}, number={3920}, isbn={978-3-540-33056-1}, address={Berlin, Heidelberg}, publisher={Springer Berlin Heidelberg}, series={Lecture Notes in Computer Science}, booktitle={Tools and Algorithms for the Construction and Analysis of Systems}, pages={318--333}, editor={Hermanns, Holger and Palsberg, Jens}, author={Leue, Stefan and Wei, Wei} }

<rdf:RDF xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#" xmlns:bibo="http://purl.org/ontology/bibo/" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:dcterms="http://purl.org/dc/terms/" xmlns:xsd="http://www.w3.org/2001/XMLSchema#" > <rdf:Description rdf:about="https://kops.uni-konstanz.de/rdf/resource/123456789/21457"> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2013-02-08T08:04:24Z</dc:date> <dc:contributor>Leue, Stefan</dc:contributor> <dcterms:abstract xml:lang="eng">Automated termination proofs are indispensable in the mechanic verification of many program properties. While most of the recent work on automated termination proofs focuses on the construction of linear ranking functions, we develop an approach based on region graphs in which regions define subsets of variable values that have different effects on loop termination. In order to establish termination, we check whether (1) any region will be exited once it is entered, and (2) no region is entered an infinite number of times. We show the effectiveness of our proof method by experiments with Java code using a prototype implementation of our approach.</dcterms:abstract> <dc:rights>deposit-license</dc:rights> <dcterms:title>A region graph based approach to termination proofs</dcterms:title> <dcterms:issued>2006</dcterms:issued> <dc:creator>Leue, Stefan</dc:creator> <dc:creator>Wei, Wei</dc:creator> <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/21457"/> <dc:language>eng</dc:language> <dcterms:bibliographicCitation>Tools and algorithms for the construction and analysis of systems : 12th International Conference, TACAS 2006, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25 - April 2, 2006; proceedings / Holger Hermanns ... (eds.). - Berlin [u.a.] : Springer, 2006. - S. 318-333. - (Lecture notes in computer science ; 3920). - ISBN 978-3-540-33056-1</dcterms:bibliographicCitation> <dc:contributor>Wei, Wei</dc:contributor> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2013-02-08T08:04:24Z</dcterms:available> <dcterms:rights rdf:resource="http://nbn-resolving.org/urn:nbn:de:bsz:352-20140905103605204-4002607-1"/> </rdf:Description> </rdf:RDF>

Dateiabrufe seit 01.10.2014 (Informationen über die Zugriffsstatistik)

leue_214578.pdf 101

Das Dokument erscheint in:

KOPS Suche


Mein Benutzerkonto