Prove with GDPLL-WD : A Complete Proof Procedure for Recursive Data Structures

Badban, Bahareh

Prove with GDPLL-WD : A Complete Proof Procedure for Recursive Data Structures

Dateien

soft_08_07.pdfGröße: 183.37 KBDownloads: 87

Datum

2008

Autor:innen

Badban, Bahareh

Schriftenreihe

Technical Report, Chair for Software Engineering, University of Konstanz

URI (zitierfähiger Link)

http://nbn-resolving.de/urn:nbn:de:bsz:352-opus-118461

Link zur Lizenz

Urheberrechtlich geschützt

Open Access-Veröffentlichung

Open Access Green

Sammlungen

Informatik und Informationswissenschaft

Publikationstyp

Working Paper/Technical Report

Publikationsstatus

Published

Zusammenfassung

In this paper we present a terminating, sound and complete algorithm for the verification of recursively defined data structures. To mention some, nat, list and tree data types and also record are commonly used examples of such structures. Recursively defined data structures are of value for use in software verification.Many programming languages support recursive data structures. The best known example on this kind is the LISP programming language, which uses list. Our algorithm, GDPLL-WD, which is an extension of the Davis, Putnam, Logemann and Loveland (DPLL) procedure solves satisfiability problem of recursive data types through providing witness assignments.

Fachgebiet (DDC)

004 Informatik

Zitieren

ISO 690

BADBAN, Bahareh, 2008. Prove with GDPLL-WD : A Complete Proof Procedure for Recursive Data Structures

BibTex

@techreport{Badban2008Prove-6424,
  year={2008},
  series={Technical Report, Chair for Software Engineering, University of Konstanz},
  title={Prove with GDPLL-WD : A Complete Proof Procedure for Recursive Data Structures},
  number={soft-08-07},
  author={Badban, Bahareh}
}

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/6424">
    <dc:rights>terms-of-use</dc:rights>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T16:12:39Z</dc:date>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:creator>Badban, Bahareh</dc:creator>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:contributor>Badban, Bahareh</dc:contributor>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/6424/1/soft_08_07.pdf"/>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <dcterms:title>Prove with GDPLL-WD : A Complete Proof Procedure for Recursive Data Structures</dcterms:title>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T16:12:39Z</dcterms:available>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/6424/1/soft_08_07.pdf"/>
    <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/6424"/>
    <dcterms:issued>2008</dcterms:issued>
    <dc:language>eng</dc:language>
    <dc:format>application/pdf</dc:format>
    <dcterms:abstract xml:lang="eng">In this paper we present a terminating, sound and complete algorithm for the verification of recursively defined data structures. To mention some, nat, list and tree data types and also record are commonly used examples of such structures. Recursively defined data structures are of value for use in software verification.Many programming languages support recursive data structures. The best known example on this kind is the LISP programming language, which uses list. Our algorithm, GDPLL-WD, which is an extension of the Davis, Putnam, Logemann and Loveland (DPLL) procedure solves satisfiability problem of recursive data types through providing witness assignments.</dcterms:abstract>
  </rdf:Description>
</rdf:RDF>