Demos

This section collects several small projects that demonstrate more diverse uses of the BlueRock's proof automation. While the code is freely browseable here, please contact us to get access to additional per-project configurations needed to run them locally.

Point
Basics
- main.cpp
- main_cpp_proof.v
Dataclass
- main.cpp
- main_proof.v
Forward List
- test.cpp
- test_cpp_proof.v
Inlining Specifications
- inline.hpp
- inline_hpp_spec.v
Singly-linked List
Loops
- main.cpp
- main_cpp_proof.v

Demos

Contents