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
Times are displayed in 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 GrossMIT CSAIL
Media Attached File Attached
16:15
15m
Talk
Towards a Coq Specification for Generalized Algebraic Datatypes in OCaml
CoqPL
Xuanrui QiNagoya University, Jacques GarrigueNagoya University
File Attached
16:30
15m
Talk
Record Updates in Coq
CoqPL
Tej ChajedMassachusetts 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-KirilyukHarvard University, Andrew AppelPrinceton, Lennart BeringerPrinceton University
File Attached
17:15
15m
Talk
Automated Synthesis of Verified Firewalls
CoqPL
Shardul ChiplunkarMassachusetts Institute of Technology, Clément Pit-ClaudelMassachusetts Institute of Technology, USA, Adam ChlipalaMassachusetts Institute of Technology
File Attached