 Symbolic Model Checking without BDDs by Armin Biere and others

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: 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.