{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T11:45:38Z","timestamp":1759146338013},"publisher-location":"Berlin, Heidelberg","reference-count":13,"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_27","type":"book-chapter","created":{"date-parts":[[2007,5,3]],"date-time":"2007-05-03T13:16:15Z","timestamp":1178198175000},"page":"340-354","source":"Crossref","is-referenced-by-count":7,"title":["A Specification Methodology by a Collection of Compact Properties as Applied to the Intel\u00ae Itanium\u2122 Processor Bus Protocol"],"prefix":"10.1007","author":[{"given":"Kanna","family":"Shimizu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David L.","family":"Dill","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ching-Tsun","family":"Chou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,8,24]]},"reference":[{"key":"27_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_40","volume-title":"International Conference on Computer-Aided Verification","author":"A.B.G.+.0.0._.Y. Abarbanel","year":"2000","unstructured":"[ABG+00]_Y. Abarbanel, I. Beer, L. Gluhovsky, S. Keidar, and Y. Wolfsthal. FoCs-Automatic Generation of Simulation Checkers from Formal Specification. In International Conference on Computer-Aided Verification, volume 1855 of Lecture Notes in Computer Science. Springer-Verlag, 2000."},{"key":"27_CR2","unstructured":"F. Aloul and K. Sakallah. Efficient Verification of the PCI Local Bus using Boolean Satisfiability. In International Workshop on Logic Synthesis (IWLS), 2000."},{"key":"27_CR3","doi-asserted-by":"crossref","unstructured":"P. Chauhan, E. M. Clarke, Y. Lu, and D. Wang. Verifying IP-Core based System-On-Chip Designs. In Proceedings of the IEEE ASIC conference, September 1999.","DOI":"10.1109\/ASIC.1999.806467"},{"key":"27_CR4","series-title":"Lect Notes Comput Sci","volume-title":"Logic of Programs: Workshop","author":"E.M. Clarke","year":"1981","unstructured":"E.M. Clarke and E.A. Emerson. Synthesis of synchronization skeletons for branching time temporal logic. In Logic of Programs: Workshop, volume 131 of Lecture Notes in Computer Science, May 1981."},{"key":"27_CR5","doi-asserted-by":"crossref","unstructured":"[CGY+00]_E. Clarke, S. German, Y. Lu, H. Veith, and D. Wang. Executable Protocol Specification in ESL. In Proceedings of the Third International Conference of Formal Methods in Computer-Aided Design, November 2000.","DOI":"10.1007\/3-540-40922-X_13"},{"key":"27_CR6","unstructured":"Intel Corporation. Itanium Processor Bus Protocol Specification. Internal document."},{"key":"27_CR7","unstructured":"Shankar G. Govindaraju and David L. Dill. Counterexample-guided choice of projections in approximate symbolic model checking. In Proceedings of International Conference on Computer-Aided Design, November 2000. San Jose, CA."},{"issue":"9","key":"27_CR8","doi-asserted-by":"crossref","first-page":"1305","DOI":"10.1109\/5.97300","volume":"79","author":"N. Halbwachs","year":"1991","unstructured":"N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous dataflow programming language lustre. Proceedings of the IEEE, 79(9):1305\u20131320, September 1991.","journal-title":"Proceedings of the IEEE"},{"key":"27_CR9","doi-asserted-by":"crossref","unstructured":"M. Kaufmann, A. Martin, and C. Pixley. Design Constraints in Symbolic Model Checking. In International Conference on Computer-Aided Verification, 1998.","DOI":"10.1007\/BFb0028768"},{"key":"27_CR10","unstructured":"Kenneth McMillan. \n                    http:\/\/www-cad.eecs.berkeley.edu\/~kenmcmil\/smv\/."},{"key":"27_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49519-3_17","volume-title":"Proceedings of the Second International Conference, Formal Methods in Computer-Aided Design","author":"A. Mokkedem","year":"1998","unstructured":"A. Mokkedem, R. Hosabettu, and G. Gopalakrishnan. Formalization and Proof of a Solution to the PCI 2.1 Bus Transaction Ordering Problem. In Proceedings of the Second International Conference, Formal Methods in Computer-Aided Design, volume 1522 of Lecture Notes in Computer Science. Springer-Verlag, 1998."},{"key":"27_CR12","doi-asserted-by":"crossref","unstructured":"Kanna Shimizu, David L. Dill, and Alan J. Hu. Monitor-Based Formal Specification of PCI. In Proceedings of the Third International Conference of Formal Methods in Computer-Aided Design, November 2000.","DOI":"10.1007\/3-540-40922-X_21"},{"key":"27_CR13","unstructured":"PCI SIG. PCI Local Bus Specification, Revision 2.2, 12 1995."}],"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_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,16]],"date-time":"2019-02-16T07:32:03Z","timestamp":1550302323000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44798-9_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425410","9783540447986"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-44798-9_27","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}