{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:47:52Z","timestamp":1725551272903},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540001164"},{"type":"electronic","value":"9783540361268"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36126-x_13","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T17:55:19Z","timestamp":1269885319000},"page":"202-219","source":"Crossref","is-referenced-by-count":13,"title":["Exploiting Transition Locality in the Disk Based Mur\u03d5 Verifier"],"prefix":"10.1007","author":[{"given":"Giuseppe","family":"Della Penna","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Benedetto","family":"Intrigila","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Enrico","family":"Tronci","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":[[2002,11,5]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"R. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. on Computers, C-35(8), Aug 1986.","DOI":"10.1109\/TC.1986.1676819"},{"key":"13_CR2","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.","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"13_CR3","unstructured":"url: http:\/\/univaq.it\/~tronci\/cached.murphi.html ."},{"key":"13_CR4","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.","DOI":"10.1109\/ICCD.1992.276232"},{"key":"13_CR5","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of 5th International SPIN Workshop","author":"R. S. F. Lerda","year":"2000","unstructured":"R. Sisto F. Lerda. Disributed-memory model checking with spin. In Proc. of 5th International SPIN Workshop, volume 1680. LNCS, Springer, 2000."},{"issue":"5","key":"13_CR6","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"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"G. J. Holzmann. An analysis of bitstate hashing. Formal Methods in Systems Design, 1998.","DOI":"10.1023\/A:1008696026254"},{"key":"13_CR8","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.","DOI":"10.1145\/196244.196377"},{"key":"13_CR9","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":"13_CR10","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.","DOI":"10.1109\/ICCD.1993.393375"},{"key":"13_CR11","unstructured":"url: http:\/\/sprout.stanford.edu\/dill\/murphi.html ."},{"key":"13_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.","DOI":"10.1109\/ICCD.1996.563579"},{"key":"13_CR13","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.","DOI":"10.1145\/240518.240638"},{"key":"13_CR14","unstructured":"url: http:\/\/netlib.bell-labs.com\/netlib\/spin\/whatispin.html ."},{"key":"13_CR15","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":"13_CR16","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."},{"key":"13_CR17","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 (CHARME), pages 206\u2013224, 1995.","DOI":"10.1007\/3-540-60385-9_13"},{"key":"13_CR18","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.","DOI":"10.1007\/978-0-387-35079-0_21"},{"key":"13_CR19","unstructured":"url: http:\/\/verify.stanford.edu\/uli\/research.html ."},{"key":"13_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.","DOI":"10.1145\/240518.240639"},{"key":"13_CR21","series-title":"Lect Notes Comput Sci","volume-title":"IFIP WG 10.5 Advanced Research Working Conference on: Correct Hardware Design and Verification Methods (CHARME)","author":"E. Tronci","year":"2001","unstructured":"E. Tronci, G. Della Penna, B. Intrigila, and M. Venturini Zilli. Exploiting transition locality in automatic verification. In IFIP WG 10.5 Advanced Research Working Conference on: Correct Hardware Design and Verification Methods (CHARME). LNCS, Springer, Sept 2001."},{"key":"13_CR22","unstructured":"E. Tronci, G. Della Penna, B. Intrigila, and M. Venturini Zilli. A probabilistic approach to space-time trading in automatic verification of concurrent system. In Proc. of 8th IEEE Asia-Pacific Software Engineering Conference (APSEC), Macau SAR, China, Dec 2001. IEEE Computer Society Press."},{"key":"13_CR23","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.","DOI":"10.1007\/3-540-56922-7_6"}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36126-X_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T15:26:37Z","timestamp":1558970797000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36126-X_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540001164","9783540361268"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-36126-x_13","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}