Toward a verified relational database management system

Malecha, Gregory Michael ; Morrisett, Greg Gregory ; et al.

Association for Computing Machinery, 2010

Online Konferenz

Zugriff:

View record in DASH (Volltext)

We report on our experience implementing a lightweight, fully verified relational database management system (RDBMS). The functional specification of RDBMS behavior, RDBMS implementation, and proof that the implementation meets the specification are all written and verified in Coq. Our contributions include: (1) a complete specification of the relational algebra in Coq; (2) an efficient realization of that model (B+ trees) implemented with the Ynot extension to Coq; and (3) a set of simple query optimizations that are proven to respect both semantics and run-time cost. In addition to describing the design and implementation of these artifacts, we highlight the challenges we encountered formalizing them, including the choice of representation for (finite) relations of typed tuples and the challenges of reasoning about data structures with complex sharing. Our experience shows that though many challenges remain, building fully-verified systems software in Coq is within reach.

Engineering and Applied Sciences

Titel:	Toward a verified relational database management system
Autor/in / Beteiligte Person:	Malecha, Gregory Michael ; Morrisett, Greg Gregory ; Shinnar, Avraham ; Wisnesky, Ryan
Link:	View record in DASH (Volltext) http://www.eecs.harvard.edu/~ryan/
Veröffentlichung:	Association for Computing Machinery, 2010
Medientyp:	Konferenz
DOI:	10.1145/1706299.1706329
Sonstiges:	Nachgewiesen in: Digital Access to Scholarship at Harvard (DASH) Sprachen: English Collection: FAS Scholarly Articles Document Type: Conference Paper Language: English Relation: http://www.eecs.harvard.edu/~ryan/; Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '10

Klicken Sie ein Format an und speichern Sie dann die Daten oder geben Sie eine Empfänger-Adresse ein und lassen Sie sich per Email zusenden.

BibTeX Citavi, JabRef, u.a.
(Literaturverwaltung)

PDF kein Volltext!
(Merkzettel, Notizen)

RIS Endnote, Citavi u.a.
(Literaturverwaltung)

MODS
(XML zur Weiterverarbeitung)

oder

Wählen Sie das für Sie passende Zitationsformat und kopieren Sie es dann in die Zwischenablage, lassen es sich per Mail zusenden oder speichern es als PDF-Datei.

Gewünschter Zitations-Stil:

oder

Bitte prüfen Sie, ob die Zitation formal korrekt ist, bevor Sie sie in einer Arbeit verwenden. Benutzen Sie gegebenenfalls den "Exportieren"-Dialog, wenn Sie ein Literaturverwaltungsprogramm verwenden und die Zitat-Angaben selbst formatieren wollen.