{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T06:59:09Z","timestamp":1779087549074,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540412199","type":"print"},{"value":"9783540409229","type":"electronic"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-40922-x_23","type":"book-chapter","created":{"date-parts":[[2007,11,29]],"date-time":"2007-11-29T04:41:36Z","timestamp":1196311296000},"page":"409-426","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":60,"title":["SAT-Based Verification without State Space Traversal"],"prefix":"10.1007","author":[{"given":"Per","family":"Bjesse","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Koen","family":"Claessen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,6,18]]},"reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"P. A. Abdulla, P. Bjesse, and N. E\u00e9n. Symbolic reachability analysis based on SAT-solvers. In Proc. TACAS \u201900, 9\n                           \n                    th\n                  \n                           Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, 2000.","DOI":"10.1007\/3-540-46419-0_28"},{"key":"23_CR2","doi-asserted-by":"crossref","unstructured":"A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. TACAS\u2019 99, 8\n                           \n                    th\n                  \n                           Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, 1999.","DOI":"10.21236\/ADA360973"},{"issue":"8","key":"23_CR3","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. on Computers, C-35(8):677\u2013691, Aug. 1986.","journal-title":"IEEE Trans. on Computers"},{"key":"23_CR4","unstructured":"E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, December 1999."},{"key":"23_CR5","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: A unified model for static analysis of programs by construction or approximation of fixpoints. In Proc. 4\n                           \n                    th\n                  \n                           ACM Symp. on Principles of Programming Languages, pages 238\u2013252, 1977.","DOI":"10.1145\/512950.512973"},{"key":"23_CR6","unstructured":"C. A. J. van Eijk. Sequential equivalence checking without state space traversal. In Proc. Conf. on Design, Automation and Test in Europe, 1998."},{"key":"23_CR7","doi-asserted-by":"crossref","unstructured":"S. G. Govindaraju and D. L. Dill. Approximate symbolic model checking using overlapping projections. In Electronic Notes in Theoretical Computer Science, July 1999. Trento, Italy.","DOI":"10.21236\/ADA401014"},{"key":"23_CR8","series-title":"Lect Notes Comput Sci","volume-title":"About synchronous programming and abstract interpretation","author":"N. Halbwachs","year":"1994","unstructured":"N. Halbwachs. About synchronous programming and abstract interpretation. In B. LeCharlier, editor, International Symposium on Static Analysis, SAS\u201994, Namur, Belgium, September 1994. LNCS 864, Springer Verlag."},{"key":"23_CR9","doi-asserted-by":"crossref","unstructured":"N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous dataflow programming language Lustre. Proceedings of the IEEE, 79(9):1305\u20131320, September 1991.","DOI":"10.1109\/5.97300"},{"issue":"2","key":"23_CR10","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1023\/A:1008678014487","volume":"11","author":"N. Halbwachs","year":"1997","unstructured":"N. Halbwachs, Y. E. Proy, and P. Roumanoff. Verification of real-time systems using linear relation analysis. Formal Methods in System Design, 11(2):157\u2013185, August 1997.","journal-title":"Formal Methods in System Design"},{"key":"23_CR11","doi-asserted-by":"crossref","unstructured":"Z. Manna and the STeP group. STeP: The Stanford Temporal Prover. Technical report, Computer Science Department, Stanford University, July 1994.","DOI":"10.21236\/ADA324036"},{"key":"23_CR12","doi-asserted-by":"crossref","unstructured":"M. Sheeran, S. Singh, and G. St\u00e5lmarck. Checking safety properties using induction and a SAT-solver. In Formal Methods in Computer Aided Design, 2000.","DOI":"10.1007\/3-540-40922-X_8"},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"M. Sheeran and G. St\u00e5lmarck. A tutorial on St\u00e5lmarck\u2019s method of propositional proof. Formal Methods In System Design, 16(1), 2000.","DOI":"10.1023\/A:1008725524946"},{"key":"23_CR14","unstructured":"G. St\u00e5lmarck. A system for determining propositional logic theorems by applying values and rules to triplets that are generated from a formula. Swedish Patent No. 467076 (1992), U.S. Patent No. 5 276 897 (1994), European Patent No. 0403 454 (1995), 1989."},{"key":"23_CR15","doi-asserted-by":"crossref","unstructured":"P. F. Williams, A. Biere, E. M. Clarke, and A. Gupta. Combining decision diagrams and SAT procedures for efficient symbolic model checking. In Proc. 12\n                           \n                    th\n                  \n                           Int. Conf. on Computer Aided Verification, 2000.","DOI":"10.1007\/10722167_13"}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-40922-X_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,29]],"date-time":"2020-01-29T08:17:36Z","timestamp":1580285856000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-40922-X_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540412199","9783540409229"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-40922-x_23","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2000]]},"assertion":[{"value":"18 June 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}