{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:27:39Z","timestamp":1761611259635},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665595"},{"type":"electronic","value":"9783540481539"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48153-2_19","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T17:13:28Z","timestamp":1269882808000},"page":"250-266","source":"Crossref","is-referenced-by-count":27,"title":["Hints to Accelerate Symbolic Traversal"],"prefix":"10.1007","author":[{"given":"Kavita","family":"Ravi","sequence":"first","affiliation":[]},{"given":"Fabio","family":"Somenzi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,6,3]]},"reference":[{"issue":"2","key":"19_CR1","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M. Abadi","year":"1991","unstructured":"M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253\u2013284, 1991.","journal-title":"Theoretical Computer Science"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"A. Aziz, J. Kukula, and T. Shiple. Hybrid verification using saturated simulation. In Proc. of the Design Automation Conference, pages 615\u2013618, San Francisco, CA,June 1998.","DOI":"10.1145\/277044.277204"},{"key":"19_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/BFb0028744","volume-title":"Tenth Conference on Computer Aided Verification (CAV\u201998)","author":"I. Beer","year":"1998","unstructured":"I. Beer, S. Ben-David, and A. Landver. On-the-fly model checking of RCTL formulas. In A. J. Hu and M. Y. Vardi, editors, Tenth Conference on Computer Aided Verification (CAV\u201998), pages 184\u2013194. Springer-Verlag, Berlin, 1998. LNCS 1427."},{"key":"19_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/BFb0031812","volume-title":"Formal Methods in Computer Aided Design","author":"R. K. Brayton","year":"1996","unstructured":"R. K. Brayton et al. VIS. In Formal Methods in Computer Aided Design, pages 248\u2013256. Springer-Verlag, Berlin, November 1996. LNCS 1166."},{"issue":"8","key":"19_CR5","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, August 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"R. E. Bryant, D. L. Beatty, and C. H. Seger. Formal hardware verification by symbolic ternary trajectory evaluation. In Proc. of the Design Automation Conference, pages 397\u2013402, 1991.","DOI":"10.1145\/127601.127701"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill. Sequential circuit verification using symbolic model checking. In Proc. of the Design Automation Conference, pages 46\u201351, June 1990.","DOI":"10.1145\/123186.123223"},{"key":"19_CR8","doi-asserted-by":"publisher","first-page":"728","DOI":"10.1109\/DAC.1997.597241","volume-title":"Proc. of the Design Automation Conference","author":"G. Cabodi","year":"1997","unstructured":"G. Cabodi, P. Camurati, L. Lavagno, and S. Quer. Disjunctive partitionining and partial iterative squaring: An effective approach for symbolic traversal of large circuits. In Proc. of the Design Automation Conference, pages 728\u2013733, Anaheim, CA, June 1997."},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"G. Cabodi, P. Camurati, and S. Quer. Improved reachability analysis of large finite state machines. In Proc. of the International Conference on Computer-Aided Design, pages 354\u2013360, Santa Clara, CA, November 1996.","DOI":"10.1109\/ICCAD.1996.569819"},{"key":"19_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BFb0028741","volume-title":"Tenth Conference on Computer Aided Verification (CAV\u201998)","author":"E. M. Clarke","year":"1998","unstructured":"E. M. Clarke, E. A. Emerson, S. Jha, and A. P. Sistla. Symmetry reductions in model checking. In A. J. Hu and M. Y. Vardi, editors, Tenth Conference on Computer Aided Verification (CAV\u201998), pages 147\u2013158. Springer-Verlag, Berlin, 1998. LNCS 1427."},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by constructions or approximation of fixpoints. In Proc. of the ACM Symposium on the Principles of Programming Languages, pages 238\u2013250, 1977.","DOI":"10.1145\/512950.512973"},{"key":"19_CR12","volume-title":"International Conference on Application of Concurrency to System Design","author":"J. Desel","year":"1998","unstructured":"J. Desel and E. Kindler. Proving correctness of distributed algorithms using highlevel Petri nets: A case study. In International Conference on Application of Concurrency to System Design, Aizu, Japan, March 1998."},{"key":"19_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1007\/3-540-58179-0_63","volume-title":"Sixth Conference on Computer Aided Verification (CAV\u201994)","author":"D. Geist","year":"1994","unstructured":"D. Geist and I. Beer. Efficient model checking by automated ordering of transition relation partitions. In D. L. Dill, editor, Sixth Conference on Computer Aided Verification (CAV\u201994), pages 299\u2013310, Berlin, 1994. Springer-Verlag. LNCS 818."},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"H. Iwashita, T. Nakata, and F. Hirose. CTL model checking based on forward state traversal. In Proc. of the International Conference on Computer-Aided Design, pages 82\u201387, San Jose, CA, November 1996.","DOI":"10.1109\/ICCAD.1996.569084"},{"key":"19_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/BFb0028768","volume-title":"Tenth Conference on Computer Aided Verification (CAV\u201998)","author":"M. Kaufmann","year":"1998","unstructured":"M. Kaufmann, A. Martin, and C. Pixley. Design constraints in symbolic model checking. In A. J. Hu and M. Y. Vardi, editors, Tenth Conference on Computer Aided Verification (CAV\u201998), pages 477\u2013487. Springer-Verlag, Berlin, 1998. LNCS 1427."},{"key":"19_CR16","volume-title":"Computer-Aided Verification of Coordinating Processes","author":"R. P. Kurshan","year":"1994","unstructured":"R. P. Kurshan. Computer-Aided Verification of Coordinating Processes. Princeton University Press, Princeton, NJ, 1994."},{"key":"19_CR17","volume-title":"On the verification and reimplementation of an ATM switch fabric using VIS. Technical Report 401","author":"J. Lu","year":"1997","unstructured":"J. Lu and S. Tahar. On the verification and reimplementation of an ATM switch fabric using VIS. Technical Report 401, Concordia University, Department of Electrical and Computer Engineering, September 1997."},{"key":"19_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/BFb0028742","volume-title":"Tenth Conference on Computer Aided Verification (CAV\u201998)","author":"G. S. Manku","year":"1998","unstructured":"G. S. Manku, R. Hojati, and R. K. Brayton. Structural symmetry and model checking. In A. J. Hu and M. Y. Vardi, editors, Tenth Conference on Computer Aided Verification (CAV\u201998), pages 159\u2013171. Springer-Verlag, Berlin, 1998. LNCS 1427."},{"key":"19_CR19","volume-title":"Symbolic Model Checking","author":"K. L. McMillan","year":"1994","unstructured":"K. L. McMillan. Symbolic Model Checking. Kluwer, Boston, MA, 1994."},{"key":"19_CR20","unstructured":"K. L. McMillan. Personal Communication, February 1998."},{"key":"19_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/BFb0028738","volume-title":"Tenth Conference on Computer Aided Verification (CAV\u201998)","author":"K. L. McMillan","year":"1998","unstructured":"K. L. McMillan. Verification of an implementation of Tomasulo\u2019s algorithm by compositional model checking. In A. J. Hu and M. Y. Vardi, editors, Tenth Conference on Computer Aided Verification (CAV\u201998), pages 110\u2013121. Springer-Verlag, Berlin, 1998. LNCS 1427."},{"key":"19_CR22","doi-asserted-by":"crossref","unstructured":"A. Narayan, A. J. Isles, J. Jain, R. K. Brayton, and A. L. Sangiovanni-Vincentelli. Reachability analysis using partitioned ROBDDs. In Proc. of the International Conference on Computer-Aided Design, pages 388\u2013393, November 1997.","DOI":"10.1109\/ICCAD.1997.643565"},{"key":"19_CR23","volume-title":"IWLS95","author":"R. K. Ranjan","year":"1995","unstructured":"R. K. Ranjan, A. Aziz, R. K. Brayton, B. F. Plessier, and C. Pixley. Efficient BDD algorithms for FSM synthesis and verification. IWLS95, Lake Tahoe, CA., May 1995."},{"key":"19_CR24","doi-asserted-by":"crossref","unstructured":"K. Ravi, K. L. McMillan, T. R. Shiple, and F. Somenzi. Approximation and decomposition of decision diagrams. In Proc. of the Design Automation Conference, pages 445\u2013450, San Francisco, CA, June 1998.","DOI":"10.1145\/277044.277168"},{"key":"19_CR25","doi-asserted-by":"crossref","unstructured":"K. Ravi and F. Somenzi. High-density reachability analysis. In Proc. of the International Conference on Computer-Aided Design, pages 154\u2013158, San Jose, CA, November 1995.","DOI":"10.1109\/ICCAD.1995.480006"},{"key":"19_CR26","doi-asserted-by":"crossref","unstructured":"K. Ravi and F. Somenzi. Efficient fixpoint computation for invariant checking. In Proc. of the International Conference on Computer Design, Austin, TX, October 1999. To appear.","DOI":"10.1109\/ICCD.1999.808582"},{"key":"19_CR27","doi-asserted-by":"crossref","unstructured":"R. Rudell. Dynamic variable ordering for ordered binary decision diagrams. In Proc. of the International Conference on Computer-Aided Design, pages 42\u201347, Santa Clara, CA, November 1993.","DOI":"10.1109\/ICCAD.1993.580029"},{"key":"19_CR28","doi-asserted-by":"crossref","unstructured":"H. Touati, H. Savoj, B. Lin, R. K. Brayton, and A. Sangiovanni-Vincentelli. Implicit enumeration of finite state machines using BDD\u2019s. In Proc. of the IEEE International Conference on Computer Aided Design, pages 130\u2013133, November 1990.","DOI":"10.1109\/ICCAD.1990.129860"},{"key":"19_CR29","doi-asserted-by":"crossref","unstructured":"C. H. Yang and D. L. Dill. Validation with guided search of the state space. In Proc. of the Design Automation Conference, pages 599\u2013604, San Francisco, CA, June 1998.","DOI":"10.1145\/277044.277201"},{"key":"19_CR30","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"376","DOI":"10.1007\/3-540-63166-6_37","volume-title":"Ninth Conference on Computer Aided Verification (CAV\u201997)","author":"J. Yuan","year":"1997","unstructured":"J. Yuan, J. Shen, J. Abraham, and A. Aziz. On combining formal and informal verification. In O. Grumberg, editor, Ninth Conference on Computer Aided Verification (CAV\u201997), pages 376\u2013387. Springer-Verlag, Berlin, 1997. LNCS 1254."}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48153-2_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,25]],"date-time":"2019-02-25T09:48:34Z","timestamp":1551088114000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48153-2_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665595","9783540481539"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/3-540-48153-2_19","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}