Symbolic execution
Explores program paths with symbolic inputs and a solver to find inputs that violate an assertion.
Sub-techniques
2
| ID | Name | Description |
|---|---|---|
V1031.001 | Bounded model checking | Unroll loops to a bound and check all paths (CBMC). |
V1031.002 | Contract checking | Search for inputs that break a function's pre- and post-conditions (CrossHair). |
Craft it
- Pick small pure functions with clear contracts.
- Write contracts as assertions or type annotations.
- Run with a time budget per function in CI.
Reverse engineer it
Signs that a codebase already runs this technique, and where to read how it is configured.
- CBMC harnesses, crosshair config or contract decorators in code.