= Symbolic Model Checking without BDDs by Armin Biere and others
{title2=1999}
By <Armin Biere>, <Alessandro Cimatti>, <Edmund Clarke> and <Yunshan Zhu>. Published in Tools and Algorithms for the Construction and Analysis of Systems, volume 1579, pp. 193–207.
Author-hosted text: https://cca.informatik.uni-freiburg.de/papers/BiereCimattiClarkeZhu-TACAS99.pdf
Introduces <bounded model checking> by translating a search for a bounded <counterexample> into a <Boolean satisfiability problem>. Section 2 explains unrolling and loop closure through a worked example; §3 states infinite-path semantics; §4 gives the encoding; §5 discusses bounds.
Back to article page
