Skip to main content
Link
Menu
Expand
(external link)
Document
Search
Copy
Copied
libcmc
Home
Guide
Install and build
Your first model
Using libcmc in your project
Reference
Design
cmc(1)
libcmc(3)
cmc(7)
The model file
Background
Survey and original design
Adversarial review of actor mode
Calibration against TLC
Process mode M0: catching a bug in code written as it ships
Process mode M1: canonical state and a real search
Process mode M2: a real malloc heap, and the wall it hits
Decision: one engine, a model file, the shipping binary
Process mode M3: a model file drives the checker
Process mode M4: multi-node, the checker owns the network
Process mode M5: time is an environment action
Process mode M5b: absolute time is engine-controlled
Why libcmc
Search libcmc
Source (Codeberg)
Mirror (GitHub)
Guide
From a clone to a checked model, then into your own project.
---
Read these in order the first time.
Install and build
Your first model
Using libcmc in your project
Table of contents
Install and build
Your first model
Using libcmc in your project