{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:01:46Z","timestamp":1725483706022},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540425410"},{"type":"electronic","value":"9783540447986"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44798-9_22","type":"book-chapter","created":{"date-parts":[[2007,5,3]],"date-time":"2007-05-03T13:16:15Z","timestamp":1178198175000},"page":"259-274","source":"Crossref","is-referenced-by-count":14,"title":["Exploiting Transition Locality in Automatic Verification"],"prefix":"10.1007","author":[{"given":"Enrico","family":"Tronci","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giuseppe","family":"Della Penna","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Benedetto","family":"Intrigila","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marisa Venturini","family":"Zilli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,8,24]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"R. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. on Computers, C-35(8), Aug 1986.","key":"22_CR1","DOI":"10.1109\/TC.1986.1676819"},{"doi-asserted-by":"crossref","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, (98), 1992.","key":"22_CR2","DOI":"10.1016\/0890-5401(92)90017-A"},{"doi-asserted-by":"crossref","unstructured":"D. L. Dill, A. J. Drexler, A. J. Hu, and C. H. Yang. Protocol verification as a hardware design aid. In IEEE International Conference on Computer Design: VLSI in Computers and Processors, pages 522\u20135, 1992.","key":"22_CR3","DOI":"10.1109\/ICCD.1992.276232"},{"issue":"5","key":"22_CR4","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. J. Holzmann","year":"1997","unstructured":"G. J. Holzmann. The spin model checker. IEEE Trans. on Software Engineering, 23(5):279\u2013295, May 1997.","journal-title":"IEEE Trans. on Software Engineering"},{"doi-asserted-by":"crossref","unstructured":"G. J. Holzmann. An analysis of bitstate hashing. Formal Methods in Systems Design, 1998.","key":"22_CR5","DOI":"10.1023\/A:1008696026254"},{"doi-asserted-by":"crossref","unstructured":"A. J. Hu, G. York, and D. L. Dill. New techniques for efficient verification with implicitily conjoined bdds. In 31st IEEE Design Automation Conference, pages 276\u2013282, 1994.","key":"22_CR6","DOI":"10.1145\/196244.196377"},{"unstructured":"C. N. Ip and D. L. Dill. Better verification through symmetry. In 11th International Conference on Computer Hardware Description Languages and their Applications, pages 97\u2013111, 1993.","key":"22_CR7"},{"doi-asserted-by":"crossref","unstructured":"C. N. Ip and D. L. Dill. Efficient verification of symmetric concurrent systems. In IEEE International Conference on Computer Design: VLSI in Computers and Processors, pages 230\u2013234, 1993.","key":"22_CR8","DOI":"10.1109\/ICCD.1993.393375"},{"doi-asserted-by":"crossref","unstructured":"Heh-Tyan Liaw and Chen-Shang Lin. On the obdd-representation of general boolean functions. IEEE Trans. on Computers, C-41(6), June 1992.","key":"22_CR9","DOI":"10.1109\/12.144618"},{"unstructured":"url: http:\/\/sprout.stanford.edu\/dill\/murphi.html.","key":"22_CR10"},{"unstructured":"A. Papoulis. Probability, Random Variables and Stochastic Processes. McGraw-Hill Series in System Sciences, 1965.","key":"22_CR11"},{"unstructured":"D. A. Patterson and J. L. Hennessy. Computer Architecture A Quantitative Approach. Morgan Kaufmann, 1996.","key":"22_CR12"},{"doi-asserted-by":"crossref","unstructured":"R. K. Ranjan, J. V. Sanghavi, R. K. Brayton, and A. Sangiovanni-Vincentelli. Binary decision diagrams on network of workstations. In IEEE International Conference on Computer Design, pages 358\u2013364, 1996.","key":"22_CR13","DOI":"10.1109\/ICCD.1996.563579"},{"doi-asserted-by":"crossref","unstructured":"J. V. Sanghavi, R. K. Ranjan, R. K. Brayton, and A. Sangiovanni-Vincentelli. High performance bdd package by exploiting memory hierarchy. In 33rd IEEE Design Automation Conference, 1996.","key":"22_CR14","DOI":"10.1145\/240518.240638"},{"unstructured":"url: http:\/\/netlib.bell-labs.com\/netlib\/spin\/whatispin.html.","key":"22_CR15"},{"key":"22_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1007\/3-540-63166-6_26","volume-title":"Proc. 9th Int. Conference on Computer Aided Verification","author":"U. Stern","year":"1997","unstructured":"U. Stern and D. Dill. Parallelizing the mur\u03d5 verifier. In Proc. 9th Int. Conference on Computer Aided Verification, volume 1254, pages 256\u2013267, Haifa, Israel, 1997. LNCS, Springer."},{"key":"22_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/BFb0028743","volume-title":"Proc. 10th Int. Conference on Computer Aided Verification","author":"U. Stern","year":"1998","unstructured":"U. Stern and D. Dill. Using magnetic disk instead of main memory in the mur\u03d5 verifier. In Proc. 10th Int. Conference on Computer Aided Verification, volume 1427, pages 172\u2013183, Vancouver, BC, Canada, 1998. LNCS, Springer."},{"doi-asserted-by":"crossref","unstructured":"U. Stern and D. L. Dill. Improved probabilistic verification by hash compaction. In IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, pages 206\u2013224, 1995.","key":"22_CR18","DOI":"10.1007\/3-540-60385-9_13"},{"doi-asserted-by":"crossref","unstructured":"U. Stern and D. L. Dill. A new scheme for memory-efficient probabilistic verification. In IFIP TC6\/WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification, 1996.","key":"22_CR19","DOI":"10.1007\/978-0-387-35079-0_21"},{"unstructured":"url: http:\/\/verify.stanford.edu\/uli\/research.html.","key":"22_CR20"},{"doi-asserted-by":"crossref","unstructured":"T. Stornetta and F. Brewer. Implementation of an efficient parallel bdd package. In 33rd IEEE Design Automation Conference, pages 641\u2013644, 1996.","key":"22_CR21","DOI":"10.1145\/240518.240639"},{"doi-asserted-by":"crossref","unstructured":"Pierre Wolper and Dennis Leroy. Reliable hashing without collision detection. In Proc. 5th Int. Conference on Computer Aided Verification, pages 59\u201370, Elounda, Greece, 1993.","key":"22_CR22","DOI":"10.1007\/3-540-56922-7_6"}],"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-44798-9_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,27]],"date-time":"2019-04-27T13:34:28Z","timestamp":1556372068000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44798-9_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425410","9783540447986"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-44798-9_22","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}