Toward a verified relational database management system

DSpace/Manakin Repository

Toward a verified relational database management system

Citable link to this page

 

 
Title: Toward a verified relational database management system
Author: Malecha, Gregory Michael; Morrisett, Greg Gregory; Shinnar, Avraham; Wisnesky, Ryan

Note: Order does not necessarily reflect citation order of authors.

Citation: Malecha, Gregory, Greg Morrisett, Avraham Shinnar, and Ryan Wisnesky. 2010. “Toward a verified relational database management system.” In Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL 10, 237. Association for Computing Machinery. doi:10.1145/1706299.1706329. http://dx.doi.org/10.1145/1706299.1706329.
Full Text & Related Files:
Abstract: 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.
Published Version: doi:10.1145/1706299.1706329
Other Sources: http://www.eecs.harvard.edu/~ryan/
Terms of Use: This article is made available under the terms and conditions applicable to Other Posted Material, as set forth at http://nrs.harvard.edu/urn-3:HUL.InstRepos:dash.current.terms-of-use#LAA
Citable link to this page: http://nrs.harvard.edu/urn-3:HUL.InstRepos:11318529
Downloads of this work:

Show full Dublin Core record

This item appears in the following Collection(s)

 
 

Search DASH


Advanced Search
 
 

Submitters