{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T15:30:50Z","timestamp":1759332650767},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642017476"},{"type":"electronic","value":"9783642017483"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-01748-3_15","type":"book-chapter","created":{"date-parts":[[2009,5,21]],"date-time":"2009-05-21T04:18:28Z","timestamp":1242879508000},"page":"228-244","source":"Crossref","is-referenced-by-count":2,"title":["Hybrid BDD and All-SAT Method for Model Checking"],"prefix":"10.1007","author":[{"given":"Avi","family":"Yadgar","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Orna","family":"Grumberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Assaf","family":"Schuster","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-45657-0_19","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2002","unstructured":"McMillan, K.L.: Applying SAT methods in unbounded symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 250. Springer, Heidelberg (2002)"},{"key":"15_CR2","unstructured":"Chauhan, P., Clarke, E.M., Kroening, D.: Using SAT based image computation for reachability analysis. Technical Report CMU-CS-03-151, Carnegie Mellon University (2003)"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-540-30494-4_20","volume-title":"Formal Methods in Computer-Aided Design","author":"O. Grumberg","year":"2004","unstructured":"Grumberg, O., Schuster, A., Yadgar, A.: Memory efficient all-solutions sat solver and its application for reachability analysis. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 275\u2013289. Springer, Heidelberg (2004)"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. CACM\u00a05(7) (July 1962)","DOI":"10.1145\/368273.368557"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: 39th Design Aotomation Conference, DAC 2001 (2001)","DOI":"10.1145\/378239.379017"},{"issue":"131","key":"15_CR6","first-page":"78","volume":"6","author":"D. Plaisted","year":"2000","unstructured":"Plaisted, D.: Method for design verification of hardware and non-hardware systems. United States Patents\u00a06(131), 078 (2000)","journal-title":"United States Patents"},{"issue":"2","key":"15_CR7","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1109\/MDT.2004.1277906","volume":"21","author":"G. Parthasarathy","year":"2004","unstructured":"Parthasarathy, G., Iyer, M.K., Cheng, K.-T., Wang, L.: Safety Property Verification Using Sequential SAT and Bounded Model Checking. IEEE Des. Test\u00a021(2), 132\u2013143 (2004)","journal-title":"IEEE Des. Test"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Lu, F., Iyer, M.K., Parthasarathy, G., Wang, L.-C., Cheng, K.-T., Chen, K.-C.: An efficient sequential sat solver with improved search strategies. In: DATE (2005)","DOI":"10.1109\/DATE.2005.55"},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"Iyer, M.K., Parthasarathy, G., Cheng, K.-T.: SATORI - A Fast Sequential SAT Engine for Circuits. In: ICCAD 2003 (2003)","DOI":"10.1109\/ICCAD.2003.159706"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Kuehlmann, A.: Dynamic Transition Relation Simplification for Bounded Property Checking. In: ICCAD 2004 (2004)","DOI":"10.1109\/ICCAD.2004.1382542"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Jin, H., Somenzi, F.: Prime clauses for fast enumeration of satisfying assignments to boolean circuits. In: DAC 2005 (2005)","DOI":"10.1145\/1065579.1065775"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/3-540-40922-X_22","volume-title":"Formal Methods in Computer-Aided Design","author":"A. Gupta","year":"2000","unstructured":"Gupta, A., Yang, Z., Ashar, P., Gupta, A.: SAT-based image computation with application in reachability analysis. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 354\u2013371. Springer, Heidelberg (2000)"},{"key":"15_CR13","unstructured":"Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic model checking with partitioned transition relations. In: VLSI 1991 (1991)"},{"key":"15_CR14","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: DAC 1999 (1999)","DOI":"10.21236\/ADA360973"},{"issue":"12","key":"15_CR15","doi-asserted-by":"publisher","first-page":"1137","DOI":"10.1109\/TC.1983.1676174","volume":"32","author":"H. Fujiwara","year":"1983","unstructured":"Fujiwara, H., Shimono, T.: On the acceleration of test generation algorithms. IEEE Trans. Computers\u00a032(12), 1137\u20131144 (1983)","journal-title":"IEEE Trans. Computers"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Shtrichman, O.: Tuning SAT checkers for bounded model checking. In: CAV (2000), citeseer.nj.nec.com\/shtrichman00tuning.html","DOI":"10.1007\/10722167_36"},{"key":"15_CR17","unstructured":"Somenzi, F.: Cudd: Cu decision diagram package release (1998), citeseer.ist.psu.edu\/somenzi98cudd.html"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Heyman, T., Geist, D., Grumberg, O., Schuster, A.: A scalable parallel algorithm for reachability analysis of very large circuits. Formal Methods in System Design\u00a021(3) (2002)","DOI":"10.1023\/A:1020373206491"},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-540-45069-6_15","volume-title":"Computer Aided Verification","author":"S.K. Lahiri","year":"2003","unstructured":"Lahiri, S.K., Bryant, R.E., Cook, B.: A symbolic approach to predicate abstraction. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 141\u2013153. Springer, Heidelberg (2003)"},{"key":"15_CR20","unstructured":"Li, B., Hsiao, M.S., Sheng, S.: A novel sat all-solutions solver for efficient preimage computation. In: DATE 2004 (2004)"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Chandrasekar, K., Hsiao, M.S.: State set management for sat-based unbounded model checking. In: ICCD 2005 (2005)","DOI":"10.1109\/ICCD.2005.99"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"Ganai, M.K., Gupta, A., Ashar, P.: Efficient sat-based unbounded symbolic model checking using circuit cofactoring. In: ICCAD 2004 (2004)","DOI":"10.1109\/ICCAD.2004.1382631"},{"key":"15_CR23","unstructured":"Barrett, C., Donham, J.: Combining SAT methods with non-clausal decision heuristics. In: PDPAR 2004 (2004)"},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"Ganai, M.K., Ashar, P., Gupta, A., Zhang, L., Malik, S.: Combining Strengths of Circuit-Based and CNF-Based Algorithms for a High-Performance SAT Solver. In: DAC 2002 (2002)","DOI":"10.1109\/DAC.2002.1012722"},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"Kuehlmann, A., Ganai, M.K., Paruthi, V.: Circuit-based Boolean Reasoning. In: DAC 2001 (2001)","DOI":"10.1145\/378239.378470"},{"key":"15_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-540-27813-9_50","volume-title":"Computer Aided Verification","author":"H. Jin","year":"2004","unstructured":"Jin, H., Awedh, M., Somenzi, F.: CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 519\u2013522. Springer, Heidelberg (2004)"},{"key":"15_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"663","DOI":"10.1007\/978-3-540-30201-8_48","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2004","author":"C. Thiffault","year":"2004","unstructured":"Thiffault, C., Bacchus, F., Walsh, T.: Solving non-clausal formulas with dpll search. In: Wallace, M. (ed.) CP 2004. LNCS, vol.\u00a03258, pp. 663\u2013678. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Languages: From Formal to Natural"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-01748-3_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T04:03:10Z","timestamp":1558324990000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-01748-3_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642017476","9783642017483"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-01748-3_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}