Toward a verified relational database management system

DOI10.1145/1706299.1706329MaRDI QIDQ5255077zbMATH OpenOpenAlexWikidataFDO

Authors Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky

Publication date 11 June 2015

Published in Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL http://nrs.harvard.edu/urn-3:HUL.InstRepos:11318529

zbMATH Keywords

B+ treedependent typesrelational modelseparation logic

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Database theory (68P15) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A Coq formalisation of SQL's execution engines
• A Coq formalization of the relational data model
• On the automated verification of web applications with embedded SQL
• A formalization of SQL with nulls
• Certified Graph View Maintenance with Regular Datalog

Cited in

(13)

• A Coq formalisation of SQL's execution engines
• A formally verified, optimized monitor for metric first-order dynamic logic
• A formalization of SQL with nulls
• Certified verification of relational properties
• Extensible and efficient automation through reflective tactics
• A coordination language for databases
• Mechanizing the metatheory of mini-XQuery
• Maintaining state constraints in relational databases: a proof theoretic basis
• scientific article; zbMATH DE number 1735904 (Why is no real title available?)
• A Coq formalization of the relational data model
• scientific article; zbMATH DE number 966595 (Why is no real title available?)
• A verified implementation of \(\mathrm{B}^+\)-trees in Isabelle/HOL
• Trace-based verification of imperative programs with I/O

Describes a project that uses

Uses Software

• Coq
• ARA
• Ynot

This page was built for publication: Toward a verified relational database management system

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5255077)