ESBMC Proof Strategies Simulator

Download ESBMC

Explore the different ways ESBMC proves software. Each step highlights the source line that generated the next trace item and prints the run output up to that point. Pick a strategy and the timeline becomes that strategy's rounds:

(default, no flags) one bounded BMC run with --unwind K, stopping where a bound cuts a loop or the loop ends naturally
--falsification walks only the base case per bound, looking just for bugs
--incremental-bmc walks the base case + forward condition per bound
--k-induction adds the inductive step on top of the base case + forward condition
--k-induction-parallel runs the same k-induction rounds but each step on a separate process

main.c: current event's line highlighted

Run output (states and verdicts, printed as you step)

Timeline

What you are looking at

ESBMC compiles the program into an SMT formula and asks a solver a yes or no question. Unrolling loops to a bound k produces a path constraint c; the solver checks whether c ∧ ¬p is satisfiable, where p is the property that must hold. SAT means some execution reaches a state where the property fails, hence a bug. UNSAT means no run up to k violates p. The strategies below keep the program unchanged; they change how that formula is built at each round.

Green dots are assignments (each prints a State block with the solver's model value), grey guard evaluations, amber the unwinding cut, dark red a violated property, beige a phase verdict (UNSAT/SAT), dashed the havoc that starts an inductive step, and dark chips round/phase headers.
The base case B(k) encodes plain BMC over k unwindings and checks c ∧ ¬p, so it can only find bugs.
The forward condition F(k) re-encodes the formula, drops the property, and keeps only the unwinding assertions, asking whether every loop fully unrolls within k.
The inductive step I(k) re-encodes the loop by havocking each loop-modified variable to a fresh nondet value, assuming the entry condition, then checking the property holds k more iterations. This is how ESBMC proves unbounded safety without fully unrolling.
Rounds advance k from --base-k-step to --max-k-step in steps of --k-step; each re-runs symex with --unwind k and closes on the first round where F(k) is UNSAT. With --k-step 2 that is k = 11, not 10.
--max-inductive-step gates only I(k): rounds above the cap skip from F(k) to the next k, while B(k) and F(k) still run, so a proof via F(k) is unaffected.
--incremental-bmc runs B(k) and F(k) only, with no inductive step; if F(k) never holds before the cap, the run gives up with VERIFICATION UNKNOWN.
With K < 11 in a plain run the verdict is the unwinding assertion (or one of the two unsound outcomes under --partial-loops / --no-unwinding-assertions); with K ≥ 11 the loop exits naturally and the trace reaches the assert.

Which strategy to pick

Strategy	Strengths	Weaknesses	Use it	Avoid it
Default (no flags, `--unwind K`)	Fast, single solver call, predictable; easiest to read the trace	Must hand-pick K; only bounded (needs the unwinding assertion to be sound); does not iterate	Smoke tests, tiny or known loops, debugging one property	Loops with unknown or large bounds, proving unbounded safety
`--falsification`	Cheapest bug-hunting; auto-iterates K over bounds; only cares about refutation	Never proves anything; hits `VERIFICATION UNKNOWN` at the cap; swaps unwinding assertions for assumptions; can miss deep bugs	Finding a counterexample fast, when you only need to refute	Any correctness argument
`--incremental-bmc`	Adds the forward condition, so it proves correctness once all loops fully unroll; sound when it closes; no hand-picked K	No inductive step, so the loop must unroll to a fixed point; large or unbounded loops run out the cap to UNKNOWN	Loops with reasonable bounds; when you want an automated proof	Deep loops, properties that need induction
`--k-induction`	Adds the inductive step, so it proves unbounded safety without fully unrolling; most powerful	Slowest; the havoc step yields spurious counterexamples that do not close; harder to follow	Proving loops whose full unroll is infeasible	Bounded loops, pure bug-finding
`--k-induction-parallel`	Same proof power as k-induction; uses separate processes for better time on multicore	Same weaknesses as k-induction; adds process-spawn overhead	Large k-induction jobs with idle cores	Small problems

Default and falsification answer fast but never prove; incremental-bmc gives an automated bounded proof; k-induction (parallel) gives an unbounded proof.

Sources

ESBMC docs, Verification Algorithms: esbmc.github.io/docs/theory/verification-algorithms
ESBMC docs, Usage, Unwinding Assertions & Verification Strategies: esbmc.github.io/docs/usage
src/goto-symex/symex_goto.cpp: get_unwind, loop_bound_exceeded (master)
src/esbmc/parseoptions/bmc_strategy.cpp: the B/F/I strategy loop and give-up verdict (master)
src/esbmc/parseoptions/k_induction.cpp: phase runners, --max-inductive-step gate (master)
src/esbmc/parseoptions/command_line_options.cpp: CLI validation of the shared knobs (master)

Made with Entoli