A region graph based approach to termination proofs

Cite This

Files in this item

Checksum: 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. Available under: doi: 10.1007/11691372_21

@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:dcterms="http://purl.org/dc/terms/" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#" xmlns:bibo="http://purl.org/ontology/bibo/" xmlns:dspace="http://digital-repositories.org/ontologies/dspace/0.1.0#" xmlns:foaf="http://xmlns.com/foaf/0.1/" xmlns:void="http://rdfs.org/ns/void#" xmlns:xsd="http://www.w3.org/2001/XMLSchema#" > <rdf:Description rdf:about="https://kops.uni-konstanz.de/rdf/resource/123456789/21457"> <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <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> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/21457/1/leue_214578.pdf"/> <dcterms:title>A region graph based approach to termination proofs</dcterms:title> <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/21457/1/leue_214578.pdf"/> <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dcterms:rights rdf:resource="https://kops.uni-konstanz.de/page/termsofuse"/> <dcterms:issued>2006</dcterms:issued> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> <dc:rights>terms-of-use</dc:rights> <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> </rdf:Description> </rdf:RDF>

Downloads since Oct 1, 2014 (Information about access statistics)

leue_214578.pdf 175

This item appears in the following Collection(s)

Search KOPS


Browse

My Account