{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,17]],"date-time":"2026-02-17T11:49:07Z","timestamp":1771328947199,"version":"3.50.1"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319105741","type":"print"},{"value":"9783319105758","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-10575-8_8","type":"book-chapter","created":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T08:05:28Z","timestamp":1526630728000},"page":"219-245","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":21,"title":["BDD-Based Symbolic Model Checking"],"prefix":"10.1007","author":[{"given":"Sagar","family":"Chaki","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arie","family":"Gurfinkel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,19]]},"reference":[{"issue":"6","key":"8_CR1","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1109\/TC.1978.1675141","volume":"27","author":"S.B. Akers","year":"1978","unstructured":"Akers, S.B.: Binary decision diagrams. IEEE Trans. Comput. 27(6), 509\u2013516 (1978)","journal-title":"IEEE Trans. Comput."},{"key":"8_CR2","first-page":"283","volume-title":"Proceedings of the 31st ACM IEEE Design Automation Conference (DAC \u201994)","author":"A. Aziz","year":"1994","unstructured":"Aziz, A., Tasiran, S., Brayton, R.K.: BDD variable ordering for interacting finite state machines. In: Proceedings of the 31st ACM IEEE Design Automation Conference (DAC \u201994), pp.\u00a0283\u2013288. ACM, San Diego (1994)"},{"key":"8_CR3","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/379605.379690","volume-title":"Proceedings of the 2001 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE \u201901)","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: Bebop: a path-sensitive interprocedural dataflow engine. In: Proceedings of the 2001 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE \u201901), pp.\u00a097\u2013103. ACM, Snowbird (2001)"},{"key":"8_CR4","doi-asserted-by":"publisher","DOI":"10.1016\/S0065-2458(03)58003-2","volume-title":"Bounded Model Checking","author":"A. Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded Model Checking. Academic Press, San Diego (2003)"},{"issue":"1","key":"8_CR5","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1016\/0303-1268(76)90033-X","volume":"2","author":"R.T. Boute","year":"1976","unstructured":"Boute, R.T.: The binary decision machine as programmable controller. Euromicro Newsl. 2(1), 16\u201322 (1976). doi:10.1016\/0303-1268(76)90033-X","journal-title":"Euromicro Newsl."},{"issue":"8","key":"8_CR6","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 Trans. Comput. 35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"issue":"4","key":"8_CR7","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1109\/43.275352","volume":"13","author":"J. Burch","year":"1994","unstructured":"Burch, J., Clarke, E.M., Long, D.E., McMillan, K., Dill, D.L.: Symbolic model checking for sequential circuit verification. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 13(4), 401\u2013424 (1994)","journal-title":"IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"key":"8_CR8","first-page":"1","volume-title":"Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science (LICS \u201990)","author":"J. Burch","year":"1990","unstructured":"Burch, J., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020$10^{20}$ states and beyond. In: Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science (LICS \u201990), pp.\u00a01\u201333. IEEE, Washington (1990)"},{"key":"8_CR9","doi-asserted-by":"crossref","first-page":"306","DOI":"10.1145\/309847.309938","volume-title":"Proceedings of the 36th ACM IEEE Design Automation Conference (DAC \u201999)","author":"G. Cabodi","year":"1999","unstructured":"Cabodi, G., Camurati, P., Quer, S.: Improving symbolic traversals by means of activity profiles. In: Proceedings of the 36th ACM IEEE Design Automation Conference (DAC \u201999), pp.\u00a0306\u2013311. ACM, New Orleans (1999)"},{"issue":"5","key":"8_CR10","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1109\/43.759068","volume":"18","author":"G. Cabodi","year":"1999","unstructured":"Cabodi, G., Camurati, P., Quer, S.: Improving the efficiency of BDD-based operators by means of partitioning. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 18(5), 545\u2013556 (1999)","journal-title":"IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"key":"8_CR11","first-page":"135","volume":"9","author":"G. Cabodi","year":"2015","unstructured":"Cabodi, G., Loiacono, C., Palena, M., Pasini, P., Patti, D., Quer, S., Vendraminetto, D., Biere, A., Heljanko, K.: Hardware model checking competition 2014: an analysis and comparison of model checkers and benchmarks. J. Satisf. Boolean Model. Comput. 9, 135\u2013172 (2015)","journal-title":"J. Satisf. Boolean Model. Comput."},{"issue":"12","key":"8_CR12","doi-asserted-by":"publisher","first-page":"1465","DOI":"10.1109\/43.552080","volume":"15","author":"H. Cho","year":"1996","unstructured":"Cho, H., Hachtel, G.D., Macii, E., Plessier, B., Somenzi, F.: Algorithms for approximate FSM traversal based on state space decomposition. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 15(12), 1465\u20131478 (1996)","journal-title":"IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"key":"8_CR13","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Proceedings of the 14th International Conference on Computer Aided Verification (CAV \u201902)","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) Proceedings of the 14th International Conference on Computer Aided Verification (CAV \u201902). LNCS, vol.\u00a02404, pp.\u00a0359\u2013364. Springer, Copenhagen (2002)"},{"issue":"2","key":"8_CR14","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 finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244\u2013263 (1986)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"1","key":"8_CR15","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1023\/A:1008615614281","volume":"10","author":"E.M. Clarke","year":"1997","unstructured":"Clarke, E.M., Grumberg, O., Hamaguchi, K.: Another look at LTL model checking. Form. Methods Syst. Des. 10(1), 47\u201371 (1997)","journal-title":"Form. Methods Syst. Des."},{"key":"8_CR16","volume-title":"Model Checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"8_CR17","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/3-540-52148-8_30","volume-title":"Automatic Verification Methods for Finite State Systems","author":"O. Coudert","year":"1989","unstructured":"Coudert, O., Berthet, C., Madre, J.C.: Verification of synchronous sequential machines based on symbolic execution. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems. LNCS, vol.\u00a0407, pp.\u00a0365\u2013373. Springer, Grenoble (1989)"},{"key":"8_CR18","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1109\/ICCD.1996.563525","volume-title":"Proceedings of the 1996 International Conference on Computer Design: VLSI in Computers and Processors (ICCD \u201996)","author":"R. Hojati","year":"1996","unstructured":"Hojati, R., Krishnan, S.C., Brayton, R.K.: Early quantification and partitioned transition relations. In: Proceedings of the 1996 International Conference on Computer Design: VLSI in Computers and Processors (ICCD \u201996), pp.\u00a012\u201319. IEEE, Austin (1996)"},{"issue":"4","key":"8_CR19","doi-asserted-by":"publisher","first-page":"985","DOI":"10.1002\/j.1538-7305.1959.tb01585.x","volume":"38","author":"C.Y. Lee","year":"1959","unstructured":"Lee, C.Y.: Representation of switching circuits by binary-decision programs. Bell Labs Tech. J. 38(4), 985\u2013999 (1959)","journal-title":"Bell Labs Tech. J."},{"key":"8_CR20","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/318593.318622","volume-title":"Proceedings of the 12th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201985)","author":"O. Lichtenstein","year":"1985","unstructured":"Lichtenstein, O., Pnueli, A.: Checking that finite-state concurrent programs satisfy their linear specification. In: Proceedings of the 12th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201985), pp.\u00a097\u2013107. ACM, New Orleans (1985)"},{"key":"8_CR21","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-540-69738-1_6","volume-title":"Proceedings of the 8th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI \u201907)","author":"K.L. McMillan","year":"2007","unstructured":"McMillan, K.L.: Interpolants and symbolic model checking. In: Cook, B., Podelski, A. (eds.) Proceedings of the 8th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI \u201907), Springer-Verlag, Nice, France, January 14\u201316, 2007. LNCS, vol.\u00a04349, pp.\u00a089\u201390. Springer, New York (2007)"},{"issue":"2","key":"8_CR22","doi-asserted-by":"crossref","first-page":"156","DOI":"10.1007\/s100090100038","volume":"3","author":"S. Minato","year":"2001","unstructured":"Minato, S.: Zero-suppressed BDDs and their applications. Int. J. Softw. Tools Technol. Transf. 3(2), 156\u2013170 (2001)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"8_CR23","series-title":"LNCS","first-page":"73","volume-title":"Proceedings of the 3rd International Conference on Formal Methods in Computer-Aided Design (FMCAD \u201900)","author":"I.H. Moon","year":"2000","unstructured":"Moon, I.H., Hachtel, G.D., Somenzi, F.: Border-block triangular form and conjunction schedule in image computation. In: Hunt, W.A. Jr., Johnson, S.D. (eds.) Proceedings of the 3rd International Conference on Formal Methods in Computer-Aided Design (FMCAD \u201900). LNCS, vol.\u00a01954, pp.\u00a073\u201390. Springer, Austin (2000)"},{"key":"8_CR24","first-page":"628","volume-title":"Proceedings of the 1994 International Conference on Computer-Aided Design (ICCAD \u201994)","author":"S. Panda","year":"1994","unstructured":"Panda, S., Somenzi, F., Plessier, B.: Symmetry detection and dynamic variable ordering of decision diagrams. In: Proceedings of the 1994 International Conference on Computer-Aided Design (ICCAD \u201994), pp.\u00a0628\u2013631. IEEE, San Jose (1994)"},{"issue":"2","key":"8_CR25","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/0304-3975(76)90022-0","volume":"3","author":"D.M.R. Park","year":"1976","unstructured":"Park, D.M.R.: Finiteness is mu-ineffable. Theor. Comput. Sci. 3(2), 173\u2013181 (1976)","journal-title":"Theor. Comput. Sci."},{"key":"8_CR26","volume-title":"Proceedings of the IEEE\/ACM International Workshop on Logic Synthesis (IWLS\u201995)","author":"R.K. Ranjan","year":"1995","unstructured":"Ranjan, R.K., Aziz, A., Brayton, R.K., Plessier, B., Pixley, C.: Efficient BDD algorithms for FSM synthesis and verification. In: Proceedings of the IEEE\/ACM International Workshop on Logic Synthesis (IWLS\u201995), Lake Tahoe, CA (1995)"},{"key":"8_CR27","first-page":"154","volume-title":"Proceedings of the 1995 International Conference on Computer-Aided Design (ICCAD \u201995)","author":"K. Ravi","year":"1995","unstructured":"Ravi, K., Somenzi, F.: High-density reachability analysis. In: Proceedings of the 1995 International Conference on Computer-Aided Design (ICCAD \u201995), pp.\u00a0154\u2013158. IEEE, San Jose (1995)"},{"issue":"2","key":"8_CR28","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1016\/j.cosrev.2010.06.002","volume":"5","author":"K.Y. Rozier","year":"2011","unstructured":"Rozier, K.Y.: Linear temporal logic symbolic model checking. Comput. Sci. Rev. 5(2), 163\u2013203 (2011)","journal-title":"Comput. Sci. Rev."},{"key":"8_CR29","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1109\/ICCAD.1993.580029","volume-title":"Proceedings of the 1993 International Conference on Computer-Aided Design (ICCAD \u201993)","author":"R. Rudell","year":"1993","unstructured":"Rudell, R.: Dynamic variable ordering for ordered binary decision diagrams. In: Lightner, M.R., Jess, J.A.G. (eds.) Proceedings of the 1993 International Conference on Computer-Aided Design (ICCAD \u201993), pp.\u00a042\u201347. IEEE, Santa Clara (1993)"},{"issue":"12","key":"8_CR30","doi-asserted-by":"publisher","first-page":"713","DOI":"10.1109\/T-AIEE.1938.5057767","volume":"57","author":"C.E. Shannon","year":"1938","unstructured":"Shannon, C.E.: A symbolic analysis of relay and switching circuits. Trans. Am. Inst. Electr. Eng. 57(12), 713\u2013723 (1938)","journal-title":"Trans. Am. Inst. Electr. Eng."},{"key":"8_CR31","unstructured":"Somenzi, F.: CUDD: CU decision diagram package. http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/"},{"key":"8_CR32","first-page":"130","volume-title":"Proceedings of the 1990 International Conference on Computer-Aided Design (ICCAD \u201990)","author":"H.J. Touati","year":"1990","unstructured":"Touati, H.J., Savoj, H., Lin, B., Brayton, R.K., Sangiovanni-Vincentelli, A.L.: Implicit state enumeration of finite state machines using BDDs. In: Proceedings of the 1990 International Conference on Computer-Aided Design (ICCAD \u201990), pp.\u00a0130\u2013133. IEEE, Santa Clara (1990)"},{"key":"8_CR33","first-page":"157","volume-title":"Proceedings of the 12th International Conference on Formal Methods in Computer-Aided Design (FMCAD \u201912)","author":"J. Xu","year":"2012","unstructured":"Xu, J., Williams, M., Mony, H., Baumgartner, J.: Enhanced reachability analysis via automated dynamic netlist-based hint generation. In: Proceedings of the 12th International Conference on Formal Methods in Computer-Aided Design (FMCAD \u201912), pp.\u00a0157\u2013164. IEEE, Cambridge (2012)"}],"container-title":["Handbook of Model Checking"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10575-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,2]],"date-time":"2023-09-02T18:18:34Z","timestamp":1693678714000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10575-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319105741","9783319105758"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10575-8_8","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}