{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,22]],"date-time":"2025-05-22T05:48:53Z","timestamp":1747892933197},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642541070"},{"type":"electronic","value":"9783642541087"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54108-7_12","type":"book-chapter","created":{"date-parts":[[2014,1,15]],"date-time":"2014-01-15T05:09:36Z","timestamp":1389762576000},"page":"222-241","source":"Crossref","is-referenced-by-count":8,"title":["Automated Code Proofs on a Formal Model of the X86"],"prefix":"10.1007","author":[{"given":"Shilpi","family":"Goel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"suffix":"Jr.","given":"Warren A.","family":"Hunt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","unstructured":"Kaufmann, M., Moore, J.S.: ACL2 home page, \n                  \n                    http:\/\/www.cs.utexas.edu\/users\/moore\/acl2"},{"key":"12_CR2","unstructured":"Moore, J.S.: Mechanized Operational Semantics, \n                  \n                    http:\/\/www.cs.utexas.edu\/users\/moore\/publications\/talks\/marktoberdorf-08\/index.html"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-540-30494-4_6","volume-title":"Formal Methods in Computer-Aided Design","author":"S. Ray","year":"2004","unstructured":"Ray, S., Moore, J.S.: Proof Styles in Operational Semantics. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 67\u201381. Springer, Heidelberg (2004)"},{"key":"12_CR4","unstructured":"Swords, S.: A Verified Framework for Symbolic Execution in the ACL2 Theorem Prover. PhD thesis, Department of Computer Sciences, The University of Texas at Austin (2010)"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Boyer, R.S., Hunt Jr., W.A.: Function memoization and unique object representation for ACL2 functions. In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, pp. 81\u201389. ACM (2006)","DOI":"10.1145\/1217975.1217992"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57960-5","volume-title":"FM8501: A Verified Microprocessor","author":"W.A. Hunt Jr.","year":"1994","unstructured":"Hunt Jr., W.A.: FM8501: A Verified Microprocessor. LNCS, vol.\u00a0795. Springer, Heidelberg (1994)"},{"issue":"2","key":"12_CR7","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1023\/A:1014122630277","volume":"20","author":"J. Sawada","year":"2002","unstructured":"Sawada, J., Hunt Jr., W.A.: Verification of FM9801: An Out-of-Order Microprocessor Model with Speculative Execution, Exceptions, and Program-Modifying Capability. Formal Methods in Systems Design\u00a020(2), 187\u2013222 (2002)","journal-title":"Formal Methods in Systems Design"},{"key":"12_CR8","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/BF00243132","volume":"5","author":"J..W.A. Hunt","year":"1989","unstructured":"Hunt, J. W.A.: Microprocessor design verification. Journal of Automated Reasoning\u00a05, 429\u2013460 (1989)","journal-title":"Journal of Automated Reasoning"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Hunt Jr., W.A., Swords, S., Davis, J., Slobodova, A.: Use of Formal Verification at Centaur Technology. In: Hardin, D.S. (ed.) Design and Verification of Microprocessor Systems for High-Assurance Applications, pp. 65\u201388. Springer (2010)","DOI":"10.1007\/978-1-4419-1539-9_3"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Fox, A.: Directions in ISA specification. Interactive Theorem Proving, 338\u2013344 (2012)","DOI":"10.1007\/978-3-642-32347-8_23"},{"key":"12_CR11","unstructured":"Degenbaev, U.: Formal specification of the x86 instruction set architecture (2012)"},{"key":"12_CR12","unstructured":"Bevier, W.R.: A Verified Operating System Kernel. PhD thesis, Department of Computer Sciences, The University of Texas at Austin (1987)"},{"issue":"2","key":"12_CR13","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0898-1221(94)00215-7","volume":"29","author":"R.S. Boyer","year":"1995","unstructured":"Boyer, R.S., Kaufmann, M., Moore, J.S.: The Boyer-Moore theorem prover and its interactive enhancement. Computers & Mathematics with Applications\u00a029(2), 27\u201362 (1995)","journal-title":"Computers & Mathematics with Applications"},{"issue":"1","key":"12_CR14","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1145\/227595.227603","volume":"43","author":"R.S. Boyer","year":"1996","unstructured":"Boyer, R.S., Yu, Y.: Automated Proofs of Object Code for a Widely Used Microprocessor. Journal of the ACM\u00a043(1), 166\u2013192 (1996)","journal-title":"Journal of the ACM"},{"key":"12_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/11916277_25","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J. Matthews","year":"2006","unstructured":"Matthews, J., Moore, J.S., Ray, S., Vroon, D.: Verification condition generation via theorem proving. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 362\u2013376. Springer, Heidelberg (2006)"},{"key":"12_CR16","unstructured":"Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic. Cambridge University Press (1993)"},{"issue":"7","key":"12_CR17","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1145\/1785414.1785443","volume":"53","author":"P. Sewell","year":"2010","unstructured":"Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.O.: x86-tso: a rigorous and usable programmer\u2019s model for x86 multiprocessors. Communications of the ACM\u00a053(7), 89\u201397 (2010)","journal-title":"Communications of the ACM"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Alglave, J., Fox, A., Ishtiaq, S., Myreen, M.O., Sarkar, S., Sewell, P., Nardelli, F.Z.: The semantics of power and arm multiprocessor machine code. In: Proceedings of the 4th Workshop on Declarative Aspects of Multicore Programming, pp. 13\u201324. ACM (2009)","DOI":"10.1145\/1481839.1481842"},{"issue":"2","key":"12_CR19","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/s10817-009-9118-9","volume":"42","author":"X. Feng","year":"2009","unstructured":"Feng, X., Shao, Z., Guo, Y., Dong, Y.: Certifying low-level programs with hardware interrupts and preemptive threads. Journal of Automated Reasoning\u00a042(2), 301\u2013347 (2009)","journal-title":"Journal of Automated Reasoning"},{"key":"12_CR20","unstructured":"Dowek, G., Felty, A., Huet, G., Paulin, C., Werner, B.: The Coq Proof Assistant User Guide Version 5.6. Technical Report TR 134, INRIA (December 1991)"},{"key":"12_CR21","unstructured":"Myreen, M.O., Gordon, M.J.C., Slind, K.: Decompilation Into Logic - Improved. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 78\u201381 (2012)"},{"key":"12_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-642-22863-6_26","volume-title":"Interactive Theorem Proving","author":"A.C.J. Fox","year":"2011","unstructured":"Fox, A.C.J.: LCF-style bit-blasting in HOL4. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol.\u00a06898, pp. 357\u2013362. Springer, Heidelberg (2011)"},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"Myreen, M., Davis, J.: A verified runtime for a verified theorem prover. In: Interactive Theorem Proving, pp. 265\u2013280 (2011)","DOI":"10.1007\/978-3-642-22863-6_20"},{"key":"12_CR24","unstructured":"Kaufmann, M., Moore, J.S.: ACL2 documentation, \n                  \n                    http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/acl2-doc.html"},{"key":"12_CR25","unstructured":"Google Code: ACL2 Books Repository, \n                  \n                    http:\/\/code.google.com\/p\/acl2-books\/"},{"key":"12_CR26","unstructured":"Intel: Intel 64 and IA-32 Architectures Software Developer\u2019s Manual (January 2013), \n                  \n                    http:\/\/download.intel.com\/products\/processor\/manual\/325462.pdf"},{"key":"12_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/3-540-45587-6_3","volume-title":"Practical Aspects of Declarative Languages","author":"R.S. Boyer","year":"2002","unstructured":"Boyer, R.S., Moore, J.S.: Single-threaded Objects in ACL2. In: Adsul, B., Ramakrishnan, C.R. (eds.) PADL 2002. LNCS, vol.\u00a02257, pp. 9\u201327. Springer, Heidelberg (2002)"},{"key":"12_CR28","unstructured":"ACL2 Documentation: Abstract Stobjs, \n                  \n                    http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/current\/DEFABSSTOBJ.html"},{"key":"12_CR29","unstructured":"Goel, S., Hunt, W., Kaufmann, M.: Abstract Stobjs and Their Application to ISA Modeling. In: Gamboa, R., Davis, J. (eds.) Eleventh International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2013) (2013)"},{"key":"12_CR30","unstructured":"Hunt Jr., W.A., Kaufmann, M.: A formal model of a large memory that supports efficient execution. In: Cabodi, G., Singh, S. (eds.) Proceedings of the 12th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2012), Cambrige, UK, October 22-25 (2012)"},{"key":"12_CR31","doi-asserted-by":"crossref","unstructured":"Swords, S., Davis, J.: Bit-blasting ACL2 theorems. In: Hardin, D., Schmaltz, J. (eds.) Proceeding 10th International Workshop on the ACL2 Theorem Prover and its Applications. EPTCS, vol.\u00a070, pp. 84\u2013102 (2011)","DOI":"10.4204\/EPTCS.70.7"},{"key":"12_CR32","unstructured":"Anderson, S.: Bit Twiddling Hacks, \n                  \n                    http:\/\/graphics.stanford.edu\/~seander\/bithacks.html"},{"key":"12_CR33","unstructured":"Kaufmann, M., Hunt Jr., W.A.: Towards a formal model of the x86 ISA. Technical Report TR-12-07, Department of Computer Sciences, University of Texas at Austin (May 2012)"},{"key":"12_CR34","unstructured":"Kaufmann, M., Sumners, R.: Efficient Rewriting of Data Structures in ACL2. In: 3rd ACL2 Workshop (2002)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54108-7_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,30]],"date-time":"2020-01-30T02:59:13Z","timestamp":1580353153000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54108-7_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642541070","9783642541087"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54108-7_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}