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

Loading...
Thumbnail Image
Date
2008
Editors
Contact
Journal ISSN
Electronic ISSN
ISBN
Bibliographical data
Publisher
Series
Technical Report, Chair for Software Engineering, University of Konstanz; soft-08-07
DOI (citable link)
ArXiv-ID
International patent number
Link to the license
EU project number
Project
Open Access publication
Restricted until
Title in another language
Research Projects
Organizational Units
Journal Issue
Publication type
Working Paper/Technical Report
Publication status
Published in
Abstract
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.
Summary in another language
Subject (DDC)
004 Computer Science
Keywords
Conference
Review
undefined / . - undefined, undefined. - (undefined; undefined)
Cite This
ISO 690BADBAN, 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>
Internal note
xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter
Contact
URL of original publication
Test date of URL
Examination date of dissertation
Method of financing
Comment on publication
Alliance license
Corresponding Authors der Uni Konstanz vorhanden
International Co-Authors
Bibliography of Konstanz
Refereed