 Bounded model checking

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.^[ref]