{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,26]],"date-time":"2026-08-26T04:47:43Z","timestamp":1787719663711,"version":"build-2784847793"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540657033","type":"print"},{"value":"9783540490593","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-49059-0_14","type":"book-chapter","created":{"date-parts":[[2007,11,13]],"date-time":"2007-11-13T16:56:57Z","timestamp":1194973017000},"page":"193-207","source":"Crossref","is-referenced-by-count":792,"title":["Symbolic Model Checking without BDDs"],"prefix":"10.1007","author":[{"given":"Armin","family":"Biere","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Edmund","family":"Clarke","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yunshan","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[1999,3,12]]},"reference":[{"key":"14_CR1","series-title":"Lect Notes Comput Sci","volume-title":"International Conference on Computer-Aided Verification (CAV\u201997)","author":"A. Bor\u00e4lv","year":"1997","unstructured":"Arne Bor\u00e4lv. The industrial success of verification tools based on St\u00e5lmarck\u2019s Method. In Orna Grumberg, editor, International Conference on Computer-Aided Verification (CAV\u201997), number 1254 in LNCS. Springer-Verlag, 1997."},{"issue":"8","key":"14_CR2","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 35(8):677\u2013691, 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"14_CR3","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J. R. Burch","year":"1992","unstructured":"J. R. Burch, E. M. Clarke, and K. L. McMillan. Symbolic model checking: 1020 states and beyond. Information and Computation, 98:142\u2013170, 1992.","journal-title":"Information and Computation"},{"key":"14_CR4","series-title":"Lect Notes Comput Sci","first-page":"52","volume-title":"Proceedings of the IBM Workshop on Logics of Programs","author":"E. Clarke","year":"1981","unstructured":"E. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proceedings of the IBM Workshop on Logics of Programs, volume 131 of LNCS, pages 52\u201371. Springer-Verlag, 1981."},{"key":"14_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1007\/3-540-58179-0_72","volume-title":"Computer Aided Verification, 6th International Conference (CAV\u201994)","author":"E. Clarke","year":"1994","unstructured":"E. Clarke, O. Grumberg, and K. Hamaguchi. Another look at LTL model checking. In David L. Dill, editor, Computer Aided Verification, 6th International Conference (CAV\u201994), volume 818 of LNCS, pages 415\u2013427. Springer-Verlag, June 1994."},{"issue":"5","key":"14_CR6","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E. M. Clarke","year":"1994","unstructured":"Edmund M. Clarke, Orna Grumberg, and David E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5):1512\u20131542, 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"14_CR7","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"M. Davis and H. Putnam. A computing procedure for quantification theory. Journal of the Association for Computing Machinery, 7:201\u2013215, 1960.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"14_CR8","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"E. A. Emerson","year":"1986","unstructured":"E. A. Emerson and C.-L. Lei. Modalities for model checking: Branching time strikes back. Science of Computer Programming, 8:275\u2013306, 1986.","journal-title":"Science of Computer Programming"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"F. Giunchiglia and R. Sebastiani. Building decision procedures for modal logics from propositional decision procedures-the case study of modal K. In Proc. of the 13th Conference on Automated Deduction, Lecture Notes in Artificial Intelligence. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61511-3_115"},{"key":"14_CR10","unstructured":"D. S. Johnson and M. A. Trick, editors. The second DIMACS implementation challenge, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, 1993. (see http:\/\/dimacs.rutgers.edu\/Challenges\/ )."},{"key":"14_CR11","unstructured":"H. Kautz and B. Selman. Pushing the envelope: planning, propositional logic, and stochastic search. In Proc. AAAI\u201996, Portland, OR, 1996."},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Poceedings of the Twelfth Annual ACM Symposium on Principles of Programming Languages, pages 97\u2013107, 1985.","DOI":"10.1145\/318593.318622"},{"key":"14_CR13","unstructured":"A. J. Martin. The design of a self-timed circuit for distributed mutual exclusion. In H. Fuchs, editor, Proceedings of the 1985 Chapel Hill Conference on Very Large Scale Integration, 1985."},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"issue":"3","key":"14_CR15","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A. P. Sistla","year":"1985","unstructured":"A. P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logics. Journal of Assoc. Comput. Mach., 32(3):733\u2013749, 1985.","journal-title":"Journal of Assoc. Comput. Mach."},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"G. St\u00e5lmarck and M. S\u00e4flund. Modeling and verifying systems and software in propositional logic. In B. K. Daniels, editor, Safety of Computer Control Systems (SAFECOMP\u2019 90), pages 31\u201336. Pergamon Press, 1990.","DOI":"10.1016\/B978-0-08-040953-5.50011-8"},{"key":"14_CR17","unstructured":"P. R. Stephan, R. K. Brayton, and A. L. Sangiovanni-Vincentelli. Combinational test generation using satisfiability. Technical Report M92\/112, Departement of Electrical Engineering and Computer Science, University of California at Berkley, October 1992."},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"H. Zhang. SATO: An efficient propositional prover. In International Conference on Automated Deduction (CADE\u201997), number 1249 in LNAI, pages 272\u2013275. Springer-Verlag, 1997.","DOI":"10.1007\/3-540-63104-6_28"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49059-0_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T07:00:15Z","timestamp":1556953215000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49059-0_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540657033","9783540490593"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-49059-0_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[1999]]}}}