{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:09:45Z","timestamp":1725487785953},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540678632"},{"type":"electronic","value":"9783540446590"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44659-1_14","type":"book-chapter","created":{"date-parts":[[2007,7,21]],"date-time":"2007-07-21T13:40:26Z","timestamp":1185025226000},"page":"215-232","source":"Crossref","is-referenced-by-count":2,"title":["Verified Optimizations for the Intel IA-64 Architecture"],"prefix":"10.1007","author":[{"given":"Jim","family":"Grundy","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/3-540-58179-0_44","volume-title":"Computer Aided Verification: Proceedings of the 6th International Conference (CAV\u201994)","author":"J. R. Burch","year":"1994","unstructured":"Jerry R. Burch and David L. Dill. Automatic verification of pipelined microprocessor control. In David L. Dill, editor, Computer Aided Verification: Proceedings of the 6th International Conference (CAV\u201994), volume 818 of Lecture Notes in Computer Science, pages 68\u201380, Stanford, California, June 1994. Springer-Verlag."},{"key":"14_CR2","first-page":"40","volume-title":"Formal Methods Pacific\u201997: Proceedings of FMP\u201997","author":"M. Butler","year":"1997","unstructured":"Michael Butler, Jim Grundy, Thomas L\u00e5ngbacka, Rimvydas Ruk\u0161enas, and Joakim von Wright. The refinement calculator: proof support for program refinement. In Lindsay Groves and Steve Reeves, editors, Formal Methods Pacific\u201997: Proceedings of FMP\u201997, Discrete Mathematics and Theoretical Computer Science, pages 40\u201361, Victoria University of Wellington, New Zealand, March 1997. Springer-Verlag."},{"issue":"7","key":"14_CR3","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1109\/2.689674","volume":"31","author":"C. Dulong","year":"1998","unstructured":"Carole Dulong. The IA-64 architecture at work. Computer, 31(7):24\u201332, July 1998.","journal-title":"Computer"},{"key":"14_CR4","unstructured":"Mike Gordon. A formalization of a simplified subset of the Alpha shared memory model. \n                  http:\/\/www.cl.cam.ac.uk\/Research\/HVG\/FTP\/FTP.html#papers\n                  \n                ."},{"key":"14_CR5","volume-title":"The HOL Light Manual","author":"J. Harrison","year":"1998","unstructured":"John Harrison. The HOL Light Manual. University of Cambridge, Computer Laboratory, New Museums Site, Pembroke Street, Cambridge CB2 3QG, England, edition 1.0, May 1998."},{"key":"14_CR6","unstructured":"Intel. IA-64 application developer\u2019s architecture guide. Order number 245188, Intel Corporation, Santa Clara CA, USA, May 1999."},{"key":"14_CR7","volume-title":"Applications of Symbolic Simulation to the Verification of Microprocessors","author":"R. B. Jones","year":"1999","unstructured":"Robert Brent Jones. Applications of Symbolic Simulation to the Verification of Microprocessors. PhD thesis, Stanford University, Department of Electrical Engineering, 161 Packard, 350 Serra Mall, Stanford CA 94305, USA, August 1999."},{"key":"14_CR8","volume-title":"The HOL System Description","author":"M. Norrish","year":"2000","unstructured":"Michael Norrish and Konrad Slind. The HOL System Description. University of Cambridge, Computer Laboratory, New Museums Site, Pembroke Street, Cambridge CB2 3QG, England, hol98 Taupo-2 edition, February 2000."},{"key":"14_CR9","volume-title":"The SPARC Architecture Manual","author":"SPARC International.","year":"1992","unstructured":"SPARC International. The SPARC Architecture Manual. Prentice-Hall, New Jersey, 8th edition, 1992.","edition":"8th edition"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Joakim von Wright and Kaisa Sere. Program transformations and refinements in HOL. In Myla Archer, Jeffrey J. Joyce, Karl N. Levitt, and Phillip J. Windley, editors, The HOL Theorem Proving and its Applications: International Workshop, pages 231\u2013239, University of California at Davis, August 1991. ACM-SIGDA, IEEE Computer Society Press.","DOI":"10.1109\/HOL.1991.596290"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44659-1_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,18]],"date-time":"2019-02-18T03:58:08Z","timestamp":1550462288000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44659-1_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540678632","9783540446590"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-44659-1_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}