This paper introduces a novel technique for symbolic model checking that replaces traditional BDDs with boolean decision procedures, such as Stålmarck’s Method or the Davis & Putnam Procedure. This approach avoids the space explosion issue of BDDs, generates counterexamples faster, and sometimes speeds up the verification process. The authors introduce the concept of bounded model checking for LTL, reducing it to propositional satisfiability. They demonstrate that bounded LTL model checking can be performed without a tableau construction. The paper includes an implementation of a model checker, BMC, based on bounded model checking, and presents preliminary results showing significant performance improvements over BDD-based approaches in certain scenarios. The main advantages of the new technique include faster counterexample generation, minimal length counterexamples, reduced space usage, and the elimination of the need for manual variable ordering. The paper also discusses the translation of bounded model checking problems into propositional satisfiability problems and provides bounds on the length of counterexamples. Experimental results using a tool based on bounded model checking are presented, highlighting the effectiveness of the new technique in various benchmarks.This paper introduces a novel technique for symbolic model checking that replaces traditional BDDs with boolean decision procedures, such as Stålmarck’s Method or the Davis & Putnam Procedure. This approach avoids the space explosion issue of BDDs, generates counterexamples faster, and sometimes speeds up the verification process. The authors introduce the concept of bounded model checking for LTL, reducing it to propositional satisfiability. They demonstrate that bounded LTL model checking can be performed without a tableau construction. The paper includes an implementation of a model checker, BMC, based on bounded model checking, and presents preliminary results showing significant performance improvements over BDD-based approaches in certain scenarios. The main advantages of the new technique include faster counterexample generation, minimal length counterexamples, reduced space usage, and the elimination of the need for manual variable ordering. The paper also discusses the translation of bounded model checking problems into propositional satisfiability problems and provides bounds on the length of counterexamples. Experimental results using a tool based on bounded model checking are presented, highlighting the effectiveness of the new technique in various benchmarks.