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

Kurzanzeige
dc.contributor.authorBadban, Bahareh
dc.date.accessioned2011-03-24T16:12:39Zdeu
dc.date.available2011-03-24T16:12:39Zdeu
dc.date.issued2008deu
dc.description.abstractIn 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.eng
dc.description.versionpublished
dc.format.mimetypeapplication/pdfdeu
dc.identifier.ppn323257453deu
dc.identifier.urihttp://kops.uni-konstanz.de/handle/123456789/6424
dc.language.isoengdeu
dc.legacy.dateIssued2010deu
dc.relation.ispartofseriesTechnical Report, Chair for Software Engineering, University of Konstanzeng
dc.rightsterms-of-usedeu
dc.rights.urihttps://rightsstatements.org/page/InC/1.0/deu
dc.subject.ddc004deu
dc.titleProve with GDPLL-WD : A Complete Proof Procedure for Recursive Data Structureseng
dc.typeWORKINGPAPERdeu
dspace.entity.typePublication
kops.bibliographicInfo.seriesNumbersoft-08-07eng
kops.citation.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}
}
kops.citation.iso690BADBAN, Bahareh, 2008. Prove with GDPLL-WD : A Complete Proof Procedure for Recursive Data Structuresdeu
kops.citation.iso690BADBAN, Bahareh, 2008. Prove with GDPLL-WD : A Complete Proof Procedure for Recursive Data Structureseng
kops.citation.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>
kops.description.openAccessopenaccessgreen
kops.identifier.nbnurn:nbn:de:bsz:352-opus-118461deu
kops.opus.id11846deu
relation.isAuthorOfPublication7836390d-fc5b-4523-a272-2f8f5025bf3f
relation.isAuthorOfPublication.latestForDiscovery7836390d-fc5b-4523-a272-2f8f5025bf3f

Dateien

Originalbündel

Gerade angezeigt 1 - 1 von 1
Vorschaubild nicht verfügbar
Name:
soft_08_07.pdf
Größe:
183.37 KB
Format:
Adobe Portable Document Format
soft_08_07.pdf
soft_08_07.pdfGröße: 183.37 KBDownloads: 127

Sammlungen

Informatik und Informationswissenschaft: Publikationen