A region graph based approach to termination proofs

Kurzanzeige
dc.contributor.authorLeue, Stefan
dc.contributor.authorWei, Wei
dc.date.accessioned2013-02-08T08:04:24Zdeu
dc.date.available2013-02-08T08:04:24Zdeu
dc.date.issued2006
dc.description.abstractAutomated 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.eng
dc.description.versionpublished
dc.identifier.citationTools 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-1deu
dc.identifier.doi10.1007/11691372_21deu
dc.identifier.ppn37855722Xdeu
dc.identifier.urihttp://kops.uni-konstanz.de/handle/123456789/21457
dc.language.isoengdeu
dc.legacy.dateIssued2013-02-08deu
dc.rightsterms-of-usedeu
dc.rights.urihttps://rightsstatements.org/page/InC/1.0/deu
dc.subject.ddc004deu
dc.titleA region graph based approach to termination proofseng
dc.typeINPROCEEDINGSdeu
dspace.entity.typePublication
kops.citation.bibtex
@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}
}
kops.citation.iso690LEUE, 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_21deu
kops.citation.iso690LEUE, 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_21eng
kops.citation.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>
kops.description.openAccessopenaccessgreen
kops.flag.knbibliographytrue
kops.identifier.nbnurn:nbn:de:bsz:352-214578deu
kops.sourcefieldHERMANNS, Holger, ed., Jens PALSBERG, ed.. <i>Tools and Algorithms for the Construction and Analysis of Systems</i>. 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_21deu
kops.sourcefield.plainHERMANNS, 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_21deu
kops.sourcefield.plainHERMANNS, 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_21eng
kops.submitter.emailoleg.kozlov@uni-konstanz.dedeu
relation.isAuthorOfPublicationa0cf1380-ebf9-403b-a02e-6e97bae25ef6
relation.isAuthorOfPublication86013ecb-c2c8-4d8c-9f24-da6166bb3f33
relation.isAuthorOfPublication.latestForDiscoverya0cf1380-ebf9-403b-a02e-6e97bae25ef6
source.bibliographicInfo.fromPage318
source.bibliographicInfo.seriesNumber3920
source.bibliographicInfo.toPage333
source.contributor.editorHermanns, Holger
source.contributor.editorPalsberg, Jens
source.identifier.isbn978-3-540-33056-1
source.publisherSpringer Berlin Heidelberg
source.publisher.locationBerlin, Heidelberg
source.relation.ispartofseriesLecture Notes in Computer Science
source.titleTools and Algorithms for the Construction and Analysis of Systems

Dateien

Originalbündel

Gerade angezeigt 1 - 1 von 1
Vorschaubild nicht verfügbar
Name:
leue_214578.pdf
Größe:
411.61 KB
Format:
Adobe Portable Document Format
leue_214578.pdf
leue_214578.pdfGröße: 411.61 KBDownloads: 260

Lizenzbündel

Gerade angezeigt 1 - 1 von 1
Vorschaubild nicht verfügbar
Name:
license.txt
Größe:
1.92 KB
Format:
Plain Text
Beschreibung:
license.txt
license.txtGröße: 1.92 KBDownloads: 0

Sammlungen

Informatik und Informationswissenschaft: Publikationen