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

Publikationstyp: Working Paper/Technical Report
URI (zitierfähiger Link): http://nbn-resolving.de/urn:nbn:de:bsz:352-opus-118461
Autor/innen: Badban, Bahareh
Erscheinungsjahr: 2008
Schriftenreihe: Technical Report, Chair for Software Engineering, University of Konstanz ; soft-08-07
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
Link zur Lizenz: Deposit-Lizenz

Zitieren

Dateien zu dieser Ressource

[PDF]
Name: soft_08_07.pdf
Größe: 183.3Kb
Format: PDF
Öffnen
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:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#" xmlns:bibo="http://purl.org/ontology/bibo/" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:dcterms="http://purl.org/dc/terms/" xmlns:xsd="http://www.w3.org/2001/XMLSchema#" > <rdf:Description rdf:about="https://kops.uni-konstanz.de/rdf/resource/123456789/6424"> <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:issued>2008</dcterms:issued> <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> <dc:language>eng</dc:language> <dc:rights>deposit-license</dc:rights> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T16:12:39Z</dcterms:available> <dc:format>application/pdf</dc:format> <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 93

Das Dokument erscheint in:

KOPS Suche


Stöbern

Mein Benutzerkonto