Skip to content
Documentation
Development
Operational Models

Operational Models

Operational models (OMs) are ESBMC’s hand-written models of C/C++ library and runtime behaviour, compiled to GOTO so the verifier can reason about programs that call them. These guides cover writing, fixing, and tracking OMs.

Internal C and C++ Operational Models
How ESBMC’s internal C and C++ operational models work.
Fixing Guidelines
Diagnosing and fixing operational-model bugs.
Workload Estimate and Tracking
Tracking the operational-model implementation effort.