Awesome Reviewers

Verification · Formal

Symbolic execution

Explores program paths with symbolic inputs and a solver to find inputs that violate an assertion.

Sub-techniques

  • Bounded model checking V1031.001

    Unroll loops to a bound and check all paths (CBMC).

  • Contract checking V1031.002

    Search for inputs that break a function's pre- and post-conditions (CrossHair).

How to build it

  1. Pick small pure functions with clear contracts.
  2. Write contracts as assertions or type annotations.
  3. Run with a time budget per function in CI.

Signals in a repository

  • CBMC harnesses, crosshair config or contract decorators in code.