Publikation: A region graph based approach to termination proofs
Lade...
Dateien
Datum
2006
Autor:innen
Herausgeber:innen
ISSN der Zeitschrift
Electronic ISSN
ISBN
Bibliografische Daten
Verlag
Schriftenreihe
Auflagebezeichnung
URI (zitierfähiger Link)
DOI (zitierfähiger Link)
Internationale Patentnummer
Link zur Lizenz
Angaben zur Forschungsförderung
Projekt
Open Access-Veröffentlichung
Open Access Green
Core Facility der Universität Konstanz
Titel in einer weiteren Sprache
Publikationstyp
Beitrag zu einem Konferenzband
Publikationsstatus
Published
Erschienen in
HERMANNS, Holger, ed., Jens PALSBERG, ed.. Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer Berlin Heidelberg, 2006, pp. 318-333. Lecture Notes in Computer Science. 3920. ISBN 978-3-540-33056-1. Available under: doi: 10.1007/11691372_21
Zusammenfassung
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.
Zusammenfassung in einer weiteren Sprache
Fachgebiet (DDC)
004 Informatik
Schlagwörter
Konferenz
Rezension
undefined / . - undefined, undefined
Zitieren
ISO 690
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, 2006, pp. 318-333. Lecture Notes in Computer Science. 3920. ISBN 978-3-540-33056-1. Available under: doi: 10.1007/11691372_21BibTex
@inproceedings{Leue2006regio-21457,
year={2006},
doi={10.1007/11691372_21},
title={A region graph based approach to termination proofs},
number={3920},
isbn={978-3-540-33056-1},
publisher={Springer Berlin Heidelberg},
address={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: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/server/rdf/resource/123456789/21457">
<dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/21457/1/leue_214578.pdf"/>
<dc:language>eng</dc:language>
<dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2013-02-08T08:04:24Z</dcterms:available>
<dc:creator>Wei, Wei</dc:creator>
<foaf:homepage rdf:resource="http://localhost:8080/"/>
<dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
<dcterms:issued>2006</dcterms:issued>
<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:creator>Leue, Stefan</dc:creator>
<void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
<dc:contributor>Leue, Stefan</dc:contributor>
<bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/21457"/>
<dc:rights>terms-of-use</dc:rights>
<dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
<dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
<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>
<dcterms:title>A region graph based approach to termination proofs</dcterms:title>
<dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/21457/1/leue_214578.pdf"/>
<dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2013-02-08T08:04:24Z</dc:date>
<dc:contributor>Wei, Wei</dc:contributor>
</rdf:Description>
</rdf:RDF>Interner Vermerk
xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter
Prüfungsdatum der Dissertation
Finanzierungsart
Kommentar zur Publikation
Allianzlizenz
Corresponding Authors der Uni Konstanz vorhanden
Internationale Co-Autor:innen
Universitätsbibliographie
Ja
