Technique · 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).