{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,2]],"date-time":"2025-11-02T16:25:16Z","timestamp":1762100716201,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540412199"},{"type":"electronic","value":"9783540409229"}],"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_22","type":"book-chapter","created":{"date-parts":[[2007,11,29]],"date-time":"2007-11-29T09:41:36Z","timestamp":1196329296000},"page":"391-408","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":28,"title":["SAT-Based Image Computation with Application in Reachability Analysis"],"prefix":"10.1007","author":[{"given":"Aarti","family":"Gupta","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zijiang","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pranav","family":"Ashar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anubhav","family":"Gupta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,6,18]]},"reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"P. A. Abdulla, P. Bjesse, and N. Een. 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":"22_CR2","series-title":"Lect Notes Comput Sci","volume-title":"Tools and Algorithms for the Analysis and Construction of Systems (TACAS)","author":"A. Biere","year":"1999","unstructured":"A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Tools and Algorithms for the Analysis and Construction of Systems (TACAS), volume 1579 of Lecture Notes in Computer Science, 1999."},{"key":"22_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"428","DOI":"10.1007\/3-540-61474-5_95","volume-title":"VIS: A system for verification and synthesis","author":"R. K. Brayton","year":"1996","unstructured":"R. K. Brayton et al. VIS: A system for verification and synthesis. In R. Alur and T. Henzinger, editors, Proceedings of the Internation Conference on Computer-Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 428\u2013432, June 1996."},{"issue":"8","key":"22_CR4","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 Transactions on Computers, C-35(8):677\u2013691, Aug. 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"J. Burch and V. Singhal. Tight integration of combinational verification methods. In Proceedings of the International Conference on Computer-Aided Design, pages 570\u2013576, 1998.","DOI":"10.1145\/288548.289088"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"J. R. Burch, E. M. Clarke, and D. E. Long. Representing circuits more efficiently in symbolic model checking. In Proceedings of the 28th Design Automation Conference, pages 403\u2013407, June 1991.","DOI":"10.1145\/127601.127702"},{"issue":"4","key":"22_CR7","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1109\/43.275352","volume":"13","author":"J. R. Burch","year":"1994","unstructured":"J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, and D. L. Dill. Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design, 13(4):401\u2013424, Apr. 1994.","journal-title":"IEEE Transactions on Computer-Aided Design"},{"issue":"5","key":"22_CR8","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1109\/43.759068","volume":"18","author":"G. Cabodi","year":"1999","unstructured":"G. Cabodi, P. Camurati, and S. Quer. Improving the efficiency of BDD-based operators by means of partitioning. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 18(5):545\u2013556, May 1999.","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"22_CR9","series-title":"Lect Notes Comput Sci","first-page":"365","volume-title":"Verification of synchronous sequential machines using symbolic execution","author":"O. Coudert","year":"1989","unstructured":"O. Coudert, C. Berthet, and J. C. Madre. Verification of synchronous sequential machines using symbolic execution. In Proceedings of the Internatiocal Workshop on Automatic VerificationMethods for Finite State Systems, volume 407 of Lecture Notes in Computer Science, pages 365\u2013373, June 1989."},{"key":"22_CR10","doi-asserted-by":"publisher","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 ACM, 7:201\u2013205, 1960.","journal-title":"Journal of the ACM"},{"key":"22_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1007\/3-540-58179-0_63","volume-title":"Efficient model checking by automatic ordering of transition relation partitions","author":"D. Geist","year":"1994","unstructured":"D. Geist and I. Beer. Efficient model checking by automatic ordering of transition relation partitions. In Proceedings of the Internation Conference on Computer-Aided Verification, volume 818 of Lecture Notes in Computer Science, pages 299\u2013310, 1994."},{"key":"22_CR12","unstructured":"A. Gupta and P. Ashar. Integrating a Boolean satisfiability checker and BDDs for combinational verification. In Proceedings of the VLSI Design Conference, Jan. 1998."},{"issue":"1","key":"22_CR13","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1109\/43.108614","volume":"11","author":"T. Larrabee","year":"1992","unstructured":"T. Larrabee. Test pattern generation using Boolean satisfiability. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 11(1):4\u201315, Jan. 1992.","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"22_CR14","unstructured":"J. P. Marques-Silva. Search Algorithms for Satisfiability Problems in Combinational Switching Circuits. PhD thesis, EECS Department, University of Michigan, May 1995."},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"J. P. Marques-Silva and. A. Sakallah. Grasp: A new search algorithm for satisfiability. In Proceedings of the International Conference on Computer-Aided Design, pages 220\u2013227, Nov. 1996.","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"22_CR16","unstructured":"J. P. Marquez-Silva. Grasp package. http:\/\/algos.inesc.pt\/~jpms\/software.html"},{"key":"22_CR17","doi-asserted-by":"crossref","unstructured":"I.-H. Moon, J. Kukula, K. Ravi, and F. Somenzi. To split or to conjoin: The question in image computation. In Proceedings of the Design Automation Conference, pages 23\u201328, June 2000.","DOI":"10.1145\/337292.337305"},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"A. Narayan, A. J. Isles, J. Jain, R. K. Brayton, and A. Sangiovanni-Vincentelli. Reachability analysis using partitioned ROBDDs. In Proceedings of the International Conference on Computer-Aided Design, pages 388\u2013393, 1997.","DOI":"10.1109\/ICCAD.1997.643565"},{"key":"22_CR19","unstructured":"R. K. Ranjan, A. Aziz, R. K. Brayton, B. F. Plessier, and C. Pixley. Efficient BDD algorithms for FSM synthesis and verification. In International Workshop for Logic Synthesis, May 1995. Lake Tahoe, CA."},{"key":"22_CR20","unstructured":"F. Somenzi et al. CUDD: University of Colorado Decision Diagram Package. http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/"},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"H. J. Touati, H. Savoj, B. Lin, R. K. Brayton, and A. Sangiovanni-Vincentelli. Implicit state enumeration of finite state machines using BDDs. In Proceedings of the International Conference on Computer-Aided Design, pages 130\u2013133, 1990.","DOI":"10.1109\/ICCAD.1990.129860"},{"key":"22_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1007\/10722167_13","volume-title":"Combining decision diagrams and SAT procedures for efficient symbolic model checking","author":"P. Williams","year":"2000","unstructured":"P. Williams, A. Biere, E. M. Clarke, and A. Gupta. Combining decision diagrams and SAT procedures for efficient symbolic model checking. In Proceedings of the Internation Conference on Computer-Aided Verification, volume 1855 of Lecture Notes in Computer Science, pages 124\u2013138, 2000."}],"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_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T00:23:41Z","timestamp":1737591821000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-40922-X_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540412199","9783540409229"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-40922-x_22","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]},"assertion":[{"value":"18 June 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}