{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T02:41:39Z","timestamp":1769740899781,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540677703","type":"print"},{"value":"9783540450474","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10722167_13","type":"book-chapter","created":{"date-parts":[[2006,12,30]],"date-time":"2006-12-30T03:00:33Z","timestamp":1167447633000},"page":"124-138","source":"Crossref","is-referenced-by-count":51,"title":["Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking"],"prefix":"10.1007","author":[{"given":"Poul F.","family":"Williams","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Edmund M.","family":"Clarke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anubhav","family":"Gupta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Bjesse, P., E\u00e9n, N.: Symbolic reachability analysis based on SAT solvers. In: Tools and Algorithms for the Analysis and Construction of Systems (TACAS) (2000)","DOI":"10.1007\/3-540-46419-0_28"},{"key":"13_CR2","unstructured":"Andersen, H.R., Hulgaard, H.: Boolean expression diagrams. Information and Computation (to appear)"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Andersen, H.R., Hulgaard, H.: Boolean expression diagrams. In: IEEE Symposium on Logic in Computer Science (LICS) (July 1997)","DOI":"10.1109\/LICS.1997.614938"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Proc. ACM\/IEEE Design Automation Conference, DAC (1999)","DOI":"10.21236\/ADA360973"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, p. 193. Springer, Heidelberg (1999)"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/3-540-48683-6_8","volume-title":"Computer Aided Verification","author":"A. Biere","year":"1999","unstructured":"Biere, A., Clarke, E., Raimi, R., Zhu, Y.: Verifying safety properties of a PowerPC microprocessor using symbolic model checking without BDDs. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 60\u201371. Springer, Heidelberg (1999)"},{"key":"13_CR7","unstructured":"Brglez, F., Fujiware, H.: A neutral netlist of 10 combinational benchmarks circuits and a target translator in Fortran. In: Special Session International Symposium on Circuits and Systems (ISCAS) (1985)"},{"issue":"8","key":"13_CR8","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers\u00a035(8), 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Binary decision diagrams and beyond: Enabling technologies for formal verification. In: Proc. International Conf. Computer-Aided Design (ICCAD), November 1995, pp. 236\u2013243 (1995)","DOI":"10.1109\/ICCAD.1995.480018"},{"issue":"4","key":"13_CR10","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1109\/43.275352","volume":"13","author":"J.R. Burch","year":"1994","unstructured":"Burch, J.R., Clarke, E.M., Long, D.E., MacMillan, K.L., Dill, D.L.: Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems\u00a013(4), 401\u2013424 (1994)","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"issue":"2","key":"13_CR11","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Information and Computation \u00a098(2), 142\u2013170 (1992)","journal-title":"Information and Computation"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NUSMV: A new symbolic model verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 495\u2013499. Springer, Heidelberg (1999)","DOI":"10.1007\/3-540-48683-6_44"},{"issue":"2","key":"13_CR13","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finitestate concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems\u00a08(2), 244\u2013263 (1986)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Hulgaard, H., Williams, P.F., Andersen, H.R.: Equivalence checking of combinational circuits using boolean expression diagrams. IEEE Transactions on Computer Aided Design (July 1999)","DOI":"10.1109\/43.771175"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers\u00a048 (1999)","DOI":"10.1109\/12.769433"},{"key":"13_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"13_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-49519-3_7","volume-title":"Formal Methods in Computer-Aided Design","author":"M. Sheeran","year":"1998","unstructured":"Sheeran, M., St\u00e5lmarck, G.: A tutorial on st\u00e5lmarck\u2019s proof procedure for propositional logic. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol.\u00a01522, pp. 82\u201399. Springer, Heidelberg (1998)"},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1007\/3-540-63104-6_28","volume-title":"Automated Deduction - CADE-14","author":"H. Zhang","year":"1997","unstructured":"Zhang, H.: SATO: An efficient propositional prover. In: McCune, W. (ed.) CADE 1997. LNCS, vol.\u00a01249, pp. 272\u2013275. Springer, Heidelberg (1997)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10722167_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T11:48:48Z","timestamp":1556020128000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10722167_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540677703","9783540450474"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/10722167_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2000]]}}}