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.)
| Type of Publication: | Working Paper/Technical Report |
| URI (citable link): | http://nbn-resolving.de/urn:nbn:de:bsz:352-opus-118461 |
| Author: | Badban, Bahareh |
| Year of publication: | 2008 |
| Series: | Technical Report, Chair for Software Engineering, University of Konstanz ; soft-08-07 |
| Summary: |
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.
|
| Subject (DDC): | 004 Computer Science |
| Link to License: | In Copyright |
Cite This
Files in this item
![[PDF]](/themes/Kops/images/mimes/pdf.png "PDF file"){kind=small}
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
