Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Tue 19 Jan 2021 17:00 - 17:15 at CoqPL - Contributed Talks

Insertion and retrieval operations in a relational database can be made more efficient using ordered indexes. The query planner decides which implementation of an ordered index to use for optimal performance. Ideally, the user should have access to a general ordered index API without being exposed to specific implementations of the index. Furthermore, each index implementation must provide consistent guarantees about the functions exposed through the API. Our main contribution in this work is a formally verified ordered index instance, which uses a B+-tree with Cursors as its underlying data structure. A secondary contribution is our approach to verifying modular, imperative C code. We accomplish these goals as follows. First, we define a general ordered index API. Then, we use the existing implementation of a B+-tree with Cursors (verified in previous work w.r.t. a B+-tree specification) to instantiate the general API and produce a B+-tree ordered index instance. Finally, we wrap up the B+-tree index instance as a Verified Software Unit. This final step allows us to make guarantees about functions exported by the module, and ensure that no unnecessary elements are exposed to the user. Our code is verified in the Coq Proof Assistant, using the tools Verified Software Toolchain (VST) and CompCert.

Abstract (coqpl21-final4.pdf)408KiB

Tue 19 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 17:30
Contributed TalksCoqPL at CoqPL
16:00
15m
Talk
A Limited Case for Reification by Type Inference
CoqPL
Jason Gross MIT CSAIL
Media Attached File Attached
16:15
15m
Talk
Towards a Coq Specification for Generalized Algebraic Datatypes in OCaml
CoqPL
Xuanrui Qi Nagoya University, Jacques Garrigue Nagoya University
File Attached
16:30
15m
Talk
Record Updates in Coq
CoqPL
Tej Chajed Massachusetts Institute of Technology, USA
Media Attached File Attached
16:45
15m
Break
Break
CoqPL

17:00
15m
Talk
The B+-tree Index as a Verified Software Unit
CoqPL
Anastasiya Kravchuk-Kirilyuk Harvard University, Andrew W. Appel Princeton, Lennart Beringer Princeton University
File Attached
17:15
15m
Talk
Automated Synthesis of Verified Firewalls
CoqPL
Shardul Chiplunkar Massachusetts Institute of Technology, Clément Pit-Claudel Massachusetts Institute of Technology, USA, Adam Chlipala Massachusetts Institute of Technology
File Attached