KOPS - The Institutional Repository of the University of Konstanz

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

Aufgrund von Vorbereitungen auf eine neue Version von KOPS, können kommenden Montag und Dienstag keine Publikationen eingereicht werden. (Due to preparations for a new version of KOPS, no publications can be submitted next Monday and Tuesday.)

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

Cite This

Files in this item

Checksum: MD5:5f89bf3df655ff692e85a0990dc13974

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

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

<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/rdf/resource/123456789/6424"> <dc:rights>terms-of-use</dc:rights> <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dcterms:title>Prove with GDPLL-WD : A Complete Proof Procedure for Recursive Data Structures</dcterms:title> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T16:12:39Z</dc:date> <dc:contributor>Badban, Bahareh</dc:contributor> <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/6424"/> <dc:creator>Badban, Bahareh</dc:creator> <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/6424/1/soft_08_07.pdf"/> <dc:language>eng</dc:language> <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> <dcterms:issued>2008</dcterms:issued> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T16:12:39Z</dcterms:available> <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dc:format>application/pdf</dc:format> <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/> <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/6424/1/soft_08_07.pdf"/> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> </rdf:Description> </rdf:RDF>

Downloads since Oct 1, 2014 (Information about access statistics)

soft_08_07.pdf 166

This item appears in the following Collection(s)

Search KOPS


Browse

My Account