Theory
Theory
This section covers the theory and internals behind ESBMC: how it models programs, the proof algorithms it runs, how verification conditions are encoded for SMT solvers, and the data structures it is built on.
The primitives ESBMC adds to C for non-deterministic values, assumptions, and atomic blocks.
Bounded model checking, falsification, incremental BMC, and k-induction — how ESBMC unwinds loops and proves correctness.
Proving loops halt via ranking functions, refuting them via recurrent sets, and the reduction to a k-induction reachability check.
How ESBMC models pointers as object + offset and derives bounds, NULL, use-after-free, and leak checks.
Thread interleavings, context bounding, partial-order reduction, and data-race / deadlock detection.
Abstract interpretation that infers variable ranges and injects them as assumptions before SMT solving.
Modular assume-guarantee verification with requires / ensures / assigns and loop contracts.
The –ir integer encoding versus default bit-vectors, and a manual refinement workflow.
How symbolic execution turns a program into SSA and then into an SMT formula.
LTL property checking via Büchi automata over finite prefixes.
ESBMC’s typed, reference-counted, copy-on-write internal representation.