{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:05:55Z","timestamp":1754485555245},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540600459"},{"type":"electronic","value":"9783540494133"}],"license":[{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60045-0_63","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:36:46Z","timestamp":1330277806000},"page":"367-380","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":28,"title":["Using formal verification\/analysis methods on the critical path in system design: A case study"],"prefix":"10.1007","author":[{"given":"\u00c1sgeir Th.","family":"Eir\u00edksson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ken L.","family":"McMillan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"29_CR1","unstructured":"S. V. Adve, \u201cDesigning Memory Consistency Models For Shared-Memory Multiprocessors\u201d, Ph.D. Thesis, U of Wisconsin-Madison, 1993."},{"key":"29_CR2","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant, \u201cGraph Based Algorithms for Boolean Function Manipulation\u201d, IEEE Trans. on Comp., C-35, pp. 677\u2013681, 1986.","journal-title":"IEEE Trans. on Comp."},{"key":"29_CR3","doi-asserted-by":"crossref","unstructured":"R. E. Bryant, D. L. Beatty, and C. J. Seger, \u201cFormal Hardware Verification by Symbolic Ternary Trajectory Evaluation\u201d, Proc. 28th ACM\/IEEE Design Automation Conf., 1991","DOI":"10.1145\/127601.127701"},{"key":"29_CR4","unstructured":"E. M. Clarke, O. Grumberg, H. Hirashi, S. Jha, D.E. Long, K.L. McMillan, and L. A. Ness, \u201cVerification of the Futurebus+ cache coherence protocol\u201d, Proc. 11th Intl. Symp. on Computer. Hardware Description. Lang. and their Application, 1993"},{"key":"29_CR5","volume-title":"Reasoning about Parallel Architectures","author":"W. W. Collier","year":"1992","unstructured":"W. W. Collier, \u201cReasoning about Parallel Architectures\u201d, Prentice-Hall, Englewood Cliffs, New Jersey, 1992"},{"key":"29_CR6","doi-asserted-by":"crossref","unstructured":"M. Galles, E. Williams, \u201cPerformance Optimization, Implementation, and Verification of the SGI Challenge Multiprocessor\u201d, Hot Chips Symposium, Stanford, 1993.","DOI":"10.1109\/HICSS.1994.323177"},{"key":"29_CR7","doi-asserted-by":"crossref","unstructured":"K. Gharachorloo, D. Lenoski, J.Laudon, P. Gibbons, A. Gupta, and J. Hennessy, \u201cMemory Consistency and Event Ordering in Scalable Shared-Memory Multiprocessors\u201d, Proc. 17th Ann Int'l Symp. on Computer Architecture, ACM, pp. 15\u201326, 1990.","DOI":"10.1145\/325096.325102"},{"key":"29_CR8","unstructured":"K. Gharachorloo, S. V. Adve, A. Gupta, J. L. Hennessey, and M. D. Hill, \u201cSpecifying System Requirements for Memory Consistency Models\u201d, University of Wisconsin-Madison Comp. Sci. Tech: Report #1199."},{"key":"29_CR9","doi-asserted-by":"crossref","unstructured":"M. J. C. Gordon (ed), \u201cHOL: A Proof-Generating System for Higher-Order Logic\u201d, Kluwer SECS 35, pp. 73\u2013128, 1988.","DOI":"10.1007\/978-1-4613-2007-4_3"},{"issue":"2\/3","key":"29_CR10","first-page":"5","volume":"1","author":"A. Gupta","year":"1992","unstructured":"A. Gupta, \u201cFormal Hardware Verification Methods: A Survey\u201d, Formal Methods in System Design\u201d, Vol. 1, 2\/3, pp. 5\u201392, Oct. 1992.","journal-title":"Formal Methods in System Design"},{"key":"29_CR11","volume-title":"MIPS R10000 Microprocessor User's Manual","author":"J. Heinrich","year":"1994","unstructured":"Joe Heinrich, \u201cMIPS R10000 Microprocessor User's Manual\u201d, MIPS Technologies, Inc., 2011 N. Shoreline, Mountain View, CA, 1994"},{"key":"29_CR12","doi-asserted-by":"crossref","unstructured":"R. P. Kurshan, \u201cComputer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach\u201d, Princeton University Press, 1994","DOI":"10.1515\/9781400864041"},{"key":"29_CR13","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1109\/2.121510","volume":"25","author":"D. Lenoski","year":"1992","unstructured":"D. Lenoski, J. Laudon, K. Gharachorloo, W.-D Weber, A. Gupta, J. Hennessy, M. Horowitz, M. Lam, \u201cThe Stanford Dash Multiprocessor\u201d, IEEE Computer, vol. 25, pp. 63\u201379, March 1992.","journal-title":"IEEE Computer"},{"key":"29_CR14","unstructured":"D. E. Long, \u201cModel Checking, Abstraction and Compositional Verification\u201d, Ph.D. Thesis, CMU 1993"},{"key":"29_CR15","unstructured":"K. L. McMillan, J. Schwalbe, \u201cFormal Verification of the Encore Gigamax cache consistency protocol.\u201d, Int. Symposium on Shared Memory Multiprocessors, 1991."},{"key":"29_CR16","doi-asserted-by":"crossref","unstructured":"K. L. McMillan, \u201cSymbolic Model Checking\u201d, Kluwer Academic Publishers, 1993","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"29_CR17","unstructured":"C. J. Seger, R. E. Bryant, \u201cFormal Verification by Symbolic Evaluation of Partially-Ordered Trajectories\u201d, Tech. Report 93-8, Dept. of Computer Science, University of British Columbia, Aug. 1993."},{"key":"29_CR18","unstructured":"A. S. Tanenbaum, \u201cDistributed Operating Systems\u201d, Prentice-Hall, 1995"},{"key":"29_CR19","volume-title":"Formal Verification of Hardware Design","author":"M. Yoeli","year":"1990","unstructured":"M. Yoeli, \u201cFormal Verification of Hardware Design\u201d, IEEE Computer Society Press, Los Alamitos, CA 1990."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60045-0_63","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T12:20:02Z","timestamp":1558268402000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60045-0_63"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540600459","9783540494133"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-60045-0_63","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]},"assertion":[{"value":"31 May 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}