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
Technical Report, Chair for Software Engineering, University of Konstanz; soft-06-01
Auflagebezeichnung
URI (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
Working Paper/Technical Report
Publikationsstatus
Published
Erschienen in
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 ProofsBibTex
@techreport{Leue2006Regio-5497,
year={2006},
series={Technical Report, Chair for Software Engineering, University of Konstanz},
title={A Region Graph Based Approach to Termination Proofs},
number={soft-06-01},
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/5497">
<void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
<dc:rights>terms-of-use</dc:rights>
<dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:55:52Z</dcterms:available>
<dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/5497/1/A_Region_Graph_Based_Approach_to_Termination_Proofs.pdf"/>
<dc:format>application/pdf</dc:format>
<bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/5497"/>
<dc:creator>Leue, Stefan</dc:creator>
<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:language>eng</dc:language>
<dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/5497/1/A_Region_Graph_Based_Approach_to_Termination_Proofs.pdf"/>
<dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
<dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:55:52Z</dc:date>
<dcterms:issued>2006</dcterms:issued>
<dcterms:title>A Region Graph Based Approach to Termination Proofs</dcterms:title>
<dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
<foaf:homepage rdf:resource="http://localhost:8080/"/>
<dc:contributor>Wei, Wei</dc:contributor>
<dc:creator>Wei, Wei</dc:creator>
<dc:contributor>Leue, Stefan</dc:contributor>
<dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
</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
