Verifying C++ Code with BlueRock
This field-guide is designed to help you become familiar with specifying and verifying C++ programs using the BlueRock Security FM tools. This guide is not meant to teach research level depth in separation logic or program verification and will generally avoid deep technical content. Interested readers should check out the Further Reading pages for more information.
Getting Started
These docs are designed to let you focus on what is most important to you, whether it be reasoning about classes or control flow, capturing sharing patterns, or working with collections.
- Getting Started
- For a first taste of verifying C++ programs, take a look at the quickstart guide. This will walk you through using the tools to verify simple programs and give you the basics to start exploring.
Core Tutorials
After you get past the basics, check out these tutorials that focus on specific topics.
- Working with functions
- Learn techniques for specifying and verifying functions.
- Control Flow
- Learn how to reason about control flow.
- Specifying Classes Mechanics
- Learn how to build abstractions for classes.
Further Reading
From research articles on separation logic to understanding the basics of the Rocq Proof Assistant, check out further reading.
Contributing
If you're interested in contributing to this project, please check out the contributing section.