External Resources
While this guide aims to be a (relatively) standalone introduction to the specification infrastructure at BedRock Systems, there are a variety of supplemental resources which can help you to improve your craft:
General Rocq
- Software Foundations series
- These are undergraduate level text books that use Rocq to present the basics of programming langauge theory which includes topics such as functional programming in Rocq, programm language semantics, type systems, and verification.
- Coq in a Hurry
- Yves Bertot's tutorial can help get you started with Rocq exploring basic tactics and navigation.
Separation Logic
- FRAP
- Chapter 14 cover builds up the basics of a simple separation logic and connects it to opational semantics.
- Foundations of Separation Logic
- Arthur Charguéraud's text book teaches separation logic.
- The Iris Project
- Contains undergraduate- and graduate-level course material on Iris, the separation logic framework that BRiCk is built on. These contain a number of resources built around a simple imperative programming language and goes all the way up through advanced concepts such as reasoning about concurrent programs.
- Tutorial on Separation Logic -- Peter O'Hearn
- Slides for a tutorial on separation logic.
Program Verification
- The BRiCk Project
- BlueRock's C++ program logic.
- Verifiable C
- Resources about C program verification based on the CompCert compiler and the VST toolchain. BRiCk and the BlueRock toolchain are heavily inspired by this work.