{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T06:54:59Z","timestamp":1760079299947,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439974"},{"type":"electronic","value":"9783540456575"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45657-0_38","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T14:59:43Z","timestamp":1179586783000},"page":"471-484","source":"Crossref","is-referenced-by-count":14,"title":["Mixing Forward and Backward Traversals in Guided-Prioritized BDD-Based Verification"],"prefix":"10.1007","author":[{"given":"Gianpiero","family":"Cabodi","sequence":"first","affiliation":[]},{"given":"Sergio","family":"Nocco","sequence":"additional","affiliation":[]},{"given":"Stefano","family":"Quer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,9,20]]},"reference":[{"key":"38_CR1","doi-asserted-by":"crossref","unstructured":"A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu. Symbolic Model Checking using SAT procedures instead of BDDs. In Proc. 36th Design Automat. Conf., pages 317\u2013320, New Orleans, Louisiana, June 1999.","DOI":"10.1145\/309847.309942"},{"key":"38_CR2","series-title":"Lect Notes Comput Sci","first-page":"435","volume-title":"Proc. Computer Aided Verification","author":"F. Copty","year":"2001","unstructured":"F. Copty, L. Fix, R. Fraer, E. Giunchiglia, G. Kamhi, A. Tacchella, and M. Y. Vardi. Benefits of Bounded Model Checking at an Industrial Setting. In G\u00e9rard Berry, Hubert Comon, and Alan Finkel, editors, Proc. Computer Aided Verification, volume 2102 of LNCS, pages 435\u2013453, Paris, France, July 2001. Springer-Verlag."},{"key":"38_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/10722167_13","volume-title":"Proc. Computer Aided Verification","author":"P. F. Williams","year":"2000","unstructured":"P. F. Williams, A. Biere, E. M. Clarke, and A. Gupta. Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking. In E. Allen Emerson and A. Prasad Sistla, editors, Proc. Computer Aided Verification, volume2102 of LNCS, pages 124\u2013138, Chicago, Illinois, July 2000. Springer-Verlag."},{"key":"38_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-40922-X_22","volume-title":"Proc. Formal Methods in Computer-Aided Design","author":"A. Gupta","year":"2000","unstructured":"A. Gupta, Z. Yang, P. Ashar, and A. Gupta. SAT-Based Image Computation with Application in Reachability Analysis. In Proc. Formal Methods in Computer-Aided Design, volume 1954 of LNCS, Austin, TX, USA, 2000."},{"issue":"12","key":"38_CR5","doi-asserted-by":"crossref","first-page":"1465","DOI":"10.1109\/43.552080","volume":"15","author":"H. Cho","year":"1996","unstructured":"H. Cho, G. D. Hatchel, E. Macii, B. Plessier, and F. Somenzi. Algorithms for Approximate FSM Traversal Based on State Space Decomposition. IEEE Transactions on CAD, 15(12):1465\u20131478, December 1996.","journal-title":"IEEE Transactions on CAD"},{"key":"38_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/3-540-48153-2_19","volume-title":"Correct Hardware Design and Verification Methods (CHARME\u201999)","author":"K. Ravi","year":"1999","unstructured":"K. Ravi and F. Somenzi. Hints to Accelerate Symbolic Traversal. In Correct Hardware Design and Verification Methods (CHARME\u201999), pages 250\u2013264, Berlin, September 1999. Springer-Verlag. LNCS 1703."},{"key":"38_CR7","doi-asserted-by":"crossref","unstructured":"M. K. Ganai, A. Aziz, and A. Kuehlmann. Enhancing Simulation with BDDs and ATPG. In Proc. 36th Design Automat. Conf., pages 385\u2013390, New Orleans, LA, November 1999.","DOI":"10.1145\/309847.309965"},{"key":"38_CR8","doi-asserted-by":"crossref","unstructured":"G. Cabodi, P. Camurati, and S. Quer. Efficient State Space Pruning in Symbolic Backward Traversal. In Proc. Int\u2019l Conf. on Computer Design, pages 230\u2013235, Cambridge, Massachussetts, October 1994.","DOI":"10.1109\/ICCD.1994.331895"},{"key":"38_CR9","doi-asserted-by":"crossref","unstructured":"S. G. Govindaraju and D. L. Dill. Verification by Approximate Forward and Backward Reachability. In Proc. Int\u2019l Conf. on Computer-Aided Design, pages366\u2013370, San Jose, California, November 1998.","DOI":"10.1145\/288548.289055"},{"key":"38_CR10","doi-asserted-by":"crossref","unstructured":"K. Ravi and F. Somenzi. High-Density Reachability Analysis. In Proc. Int\u2019l Conf. on Computer-Aided Design, pages 154\u2013158, San Jose, California, November 1995.","DOI":"10.1109\/ICCAD.1995.480006"},{"issue":"5","key":"38_CR11","doi-asserted-by":"crossref","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\u2014based Operators by means of Partitioning. IEEE Transactions on CAD, 18(5):545\u2013556, May 1999.","journal-title":"IEEE Transactions on CAD"},{"issue":"9","key":"38_CR12","doi-asserted-by":"crossref","first-page":"1065","DOI":"10.1109\/43.863646","volume":"19","author":"G. Cabodi","year":"2000","unstructured":"G. Cabodi, P. Camurati, and S. Quer. Improving Symbolic Reachability Analisys by means of Activity Profiles. IEEE Transactions on CAD, 19(9):1065\u20131075, September 2000.","journal-title":"IEEE Transactions on CAD"},{"key":"38_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/10722167_30","volume-title":"Proc. Computer Aided Verification","author":"R. Fraer","year":"2000","unstructured":"R. Fraer, G. Kamhi, B. Ziv, M. Y. Vardi, and L. Fix. Prioritized Traversal: Efficient Reachability Analysis for Verification and Falsification. In E. Allen Emerson and A. Prasad Sistla, editors, Proc. Computer Aided Verification, volume 1855 of LNCS, pages 389\u2013402, Chicago, Illinois, July 2000. Springer-Verlag."},{"key":"38_CR14","doi-asserted-by":"crossref","unstructured":"I. Moon, J. Jang, G. D. Hachtel, F. Somenzi, J. Yuan, and C. Pixley. Approximate Reachability Don\u2019t Cares for CTL Model Checking. In Proc. Int\u2019l Conf. on Computer-Aided Design, pages 351\u2013358, San Jose, California, November 1998.","DOI":"10.1145\/288548.289053"},{"key":"38_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/BFb0031812","volume-title":"Proc. Formal Methods in Computer-Aided Design","author":"R. K. Brayton","year":"1996","unstructured":"R. K. Brayton et al. VIS. In Mandayam Srivas and Albert Camilleri, editors, Proc. Formal Methods in Computer-Aided Design, volume 1166 of LNCS, pages 248\u2013256, Palo Alto, California, November 1996. Springer-Verlag."},{"key":"38_CR16","doi-asserted-by":"crossref","unstructured":"G. Cabodi, P. Camurati, and S. Quer. Can BDDs compete with SAT solvers on Bounded Model Checking? In Proc. 39th Design Automat. Conf., New Orleans, Louisiana, June 2002.","DOI":"10.1145\/513918.513949"},{"key":"38_CR17","doi-asserted-by":"crossref","unstructured":"S. G. Govindaraju, D. L. Dill, A. Hu, and M. A. Horowitz. Approximate Reachability Analysis with BDDs using Overlapping Projections. In Proc. 35th Design Automat. Conf., pages 451\u2013456, San Francisco, California, June 1998.","DOI":"10.1145\/277044.277169"},{"key":"38_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1007\/3-540-44585-4_11","volume-title":"Proc. Computer Aided Verification","author":"G. Cabodi","year":"2001","unstructured":"G. Cabodi. Meta-BDDs: A Decomposed Representation for Layered Symbolic Manipulation of Boolean Functions. In G\u00e9rard Berry, Hubert Comon, and Alan Finkel, editors, Proc. Computer Aided Verification, volume 2102 of LNCS, pages118\u2013130, Paris, France, July 2001. Springer-Verlag."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45657-0_38","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T13:10:57Z","timestamp":1737033057000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45657-0_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439974","9783540456575"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-45657-0_38","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}