= Bounded model checking
{wiki}
= BMC
{c}
{synonym}
A <formal verification> method that encodes a bounded execution and a violated specification as a <Boolean satisfiability problem>. A <satisfying assignment> yields a <counterexample>. For infinite-path properties, a <lasso path> can finitely represent a repeated execution. Failure to find a <counterexample> at one finite bound alone does not prove an unbounded property.<Symbolic Model Checking without BDDs by Armin Biere and others>[§§2–4, bounded encodings; §5, bounds]{ref}
Back to article page
