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]
Symbolic Model Checking without BDDs by Armin Biere and others. §§2–4, bounded encodings; §5, bounds
Articles by others on the same topic
There are currently no matching articles.