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

Zitieren

Dateien zu dieser Ressource

Prüfsumme: 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"> <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> <dc:rights>deposit-license</dc:rights> <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dc:format>application/pdf</dc:format> <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"/> <dcterms:rights rdf:resource="http://nbn-resolving.org/urn:nbn:de:bsz:352-20140905103416863-3868037-7"/> </rdf:Description> </rdf:RDF>

Dateiabrufe seit 01.10.2014 (Informationen über die Zugriffsstatistik)

soft_08_07.pdf 100

Das Dokument erscheint in:

KOPS Suche


Stöbern

Mein Benutzerkonto