Acknowledgements

BRiCk builds on a significant amount of past work and tools.

Projects

• The RustBelt Project

• Ralf Jung (https://people.mpi-sws.org/~jung/; https://www.ralfj.de/blog/ Work on RustBelt + experience with clang => a sounding board when we have questions

• Robbert Krebbers’ PhD Disseration Formalized a sequential subset of C - CH2O - in coq => where C and C++ overlap we can use his ideas directly; if C and C++ diverge, we can modify/build-on his work.

C++ (and C) Semantics

• The C++ Standard

• CompCert Verified compiler for a large subset of real-world C => insight into how we might architect our stack as we consider the (practical) boundaries of our TCB

• The Verified Software Toolchain (VST) Building on CompCert in order to provide a framework for specifying and verifying C programs written in the appropriate subset of the language

• The Cambridge University REMS Group, especially the Cerberus project

• Robbert Krebbers’ PhD Disseration

• John Regehr

• Pascal Cuoq

Separation Logic (Iris)

• The Iris Project provides the separation logic that we build our program logic on top of.