{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,7]],"date-time":"2026-05-07T02:44:14Z","timestamp":1778121854109,"version":"3.51.4"},"publisher-location":"Cham","reference-count":112,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319486277","type":"print"},{"value":"9783319486284","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-48628-4_8","type":"book-chapter","created":{"date-parts":[[2017,3,1]],"date-time":"2017-03-01T07:45:31Z","timestamp":1488354331000},"page":"173-209","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Engineering a Formal, Executable x86 ISA Simulator for Software Verification"],"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"}]},{"given":"Matt","family":"Kaufmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,3,2]]},"reference":[{"key":"8_CR1","unstructured":"von Neumann, J.: First draft of a report on the EDVAC. IEEE Ann. Hist. Comput. 15(4), 27\u201375 (1993). \n                    http:\/\/doi.ieeecomputersociety.org\/10.1109\/85.238389"},{"issue":"345\u2013363","key":"8_CR2","first-page":"5","volume":"58","author":"AM Turing","year":"1936","unstructured":"Turing, A.M.: On computable numbers, with an application to the Entscheidungsproblem. J. Math. 58(345\u2013363), 5 (1936)","journal-title":"J. Math."},{"issue":"2","key":"8_CR3","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/85.586067","volume":"19","author":"R Rojas","year":"1997","unstructured":"Rojas, R.: Konrad Zuse\u2019s legacy: the architecture of the Z1 and Z3. Ann. Hist. Comput. IEEE 19(2), 5\u201316 (1997)","journal-title":"Ann. Hist. Comput. IEEE"},{"key":"8_CR4","unstructured":"Intel Manuals (September, 2015) Intel 64 and IA-32 Architectures Software Developer\u2019s Manuals. Order Number: 325462-056US"},{"key":"8_CR5","unstructured":"Intel (Accessed: October, 2015.) Intel Developer Zone - ISA Extensions. See \n                    https:\/\/software.intel.com\/en-us\/isa-extensions\/"},{"key":"8_CR6","unstructured":"Kaufmann, M., Moore, J.S.: (Accessed: 2015) ACL2 home page. (see \n                    http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\n                    \n                  )"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Boston (2000)","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"8_CR8","unstructured":"Boyer, R.S., Kaufmann, M., Moore, J.S.: The boyer-moore theorem prover and its interactive enhancement. Comput. Math. Appl. 29(2), 27\u201362 (1995). \n                    http:\/\/citeseerx.ist.psu.edu\/viewdoc\/summary?doi=10.1.1.51.7689"},{"key":"8_CR9","unstructured":"Sawada, J., Hunt Jr., J.W.: Verification of FM9801: an out-of-order microprocessor model with speculative execution, exceptions, and program-modifying capability. Form. Methods Syst. Des. 20(2), 187\u2013222 (2002). \n                    http:\/\/dl.acm.org\/citation.cfm?id=584665"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Hunt Jr., W.A.: FM8501: A Verified Microprocessor, LNAI, vol. 795. Springer (1994)","DOI":"10.1007\/3-540-57960-5"},{"key":"8_CR11","unstructured":"Section 2.2.10: Intel 64 Architecture, Vol. 1, Intel 64 and IA-32 Architectures Software Developer\u2019s Manual. (September, 2015) Order Number: 325462-056US"},{"key":"8_CR12","unstructured":"x86isa Books in the ACL2 Community Books Project on Github (Accessed: October, 2015). See \n                    https:\/\/github.com\/acl2\/acl2\/tree\/master\/books\/projects\/x86isa"},{"key":"8_CR13","unstructured":"x86isa ACL2 Books (Accessed: October, 2015) Documentation of the bleeding-edge ACL2-based model of the x86 ISA. \n                    http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/manuals\/current\/manual\/index.html?topic=ACL2____X86ISA"},{"key":"8_CR14","unstructured":"Bevier, W.R., Hunt Jr., W.A., Moore, J.S., Young, W.D.: Special issue on system verification. J. Autom. Reason. 5(4), 409\u2013530 (1989)"},{"key":"8_CR15","doi-asserted-by":"publisher","unstructured":"Kaufmann, M., Moore, J.S., Ray, S., Reeber, E.: Integrating external deduction tools with ACL2. J. Appl. Log. 7(1), 3\u201325 (2009). doi:\n                    10.1016\/j.jal.2007.07.002\n                    \n                  , \n                    http:\/\/www.sciencedirect.com\/science\/article\/pii\/S1570868307000602\n                    \n                  , special Issue: Empirically Successful Computerized Reasoning","DOI":"10.1016\/j.jal.2007.07.002"},{"key":"8_CR16","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). \n                    http:\/\/repositories.lib.utexas.edu\/handle\/2152\/ETD-UT-2010-12-2210"},{"key":"8_CR17","unstructured":"Glucose SAT Solver (Accessed: October, 2015). \n                    http:\/\/www.labri.fr\/perso\/lsimon\/glucose\/"},{"key":"8_CR18","unstructured":"Minisat SAT Solver (Accessed: October, 2015). \n                    http:\/\/minisat.se\/"},{"key":"8_CR19","unstructured":"ACL2 System and Books Repository on Github (Accessed: October, 2015). See \n                    https:\/\/github.com\/acl2\/acl2"},{"key":"8_CR20","unstructured":"Davis, J., Kaufmann, M.: Industrial-Strength Documentation for ACL2. EPTCS 152:9\u201325 (2014). \n                    http:\/\/www.cs.utexas.edu\/users\/kaufmann\/talks\/acl2-workshop-2014\/acl2-14-davis-kaufmann.pdf"},{"key":"8_CR21","unstructured":"Kaufmann, M., Moore, J.S.: (Accessed: October, 2015) ACL2 documentation. See \n                    http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/current\/manual\/index.html?topic=ACL2____ACL2"},{"key":"8_CR22","unstructured":"2005 ACM Software System Award (2005) The Boyer-Moore Theorem Prover. (see \n                    http:\/\/awards.acm.org\/software_system\/\n                    \n                  )"},{"key":"8_CR23","unstructured":"ACL2 Applications (Accessed: October, 2015). See \n                    http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/current\/manual\/index.html?topic=ACL2____INTERESTING-APPLICATIONS"},{"key":"8_CR24","unstructured":"Centaur Technology (Accessed: October 2015). \n                    http:\/\/www.centtech.com"},{"key":"8_CR25","unstructured":"FV Group at Centaur (Accessed: October, 2015). \n                    http:\/\/fv.centtech.com"},{"key":"8_CR26","doi-asserted-by":"publisher","unstructured":"Davis, J., Slobodova, A., Swords, S.: Microcode verification \u2014 another piece of the microprocessor verification puzzle. In: Klein, G., Gamboa, R. (eds.) Interactive Theorem Proving, Lecture Notes in Computer Science, vol. 8558, pp. 1\u201316. Springer International Publishing (2014). doi:\n                    10.1007\/978-3-319-08970-6_1","DOI":"10.1007\/978-3-319-08970-6_1"},{"key":"8_CR27","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). \n                    https:\/\/www.cs.utexas.edu\/~jared\/publications\/2010-hardin-centaur.pdf"},{"key":"8_CR28","unstructured":"Flatau, A., Kaufmann, M., Reed, D.F., Russinoff, D., Smith, E.W., Sumners, R.: Formal verification of microprocessors at AMD. In: 4th International Workshop on Designing Correct Circuits (DCC 2002), Grenoble, France (2002)"},{"key":"8_CR29","doi-asserted-by":"crossref","unstructured":"Russinoff, D.M.: A case study in formal verification of register-transfer logic with ACL2: the floating point adder of the AMD athlon TM processor. In: Formal Methods in Computer-Aided Design, pp. 22\u201355. Springer (2000)","DOI":"10.1007\/3-540-40922-X_3"},{"issue":"5","key":"8_CR30","doi-asserted-by":"publisher","first-page":"900","DOI":"10.1109\/TC.2012.40","volume":"62","author":"David Russinoff","year":"2013","unstructured":"Russinoff, David: Computation and formal verification of SRT quotient and square root digit selection tables. IEEE Trans. Comput. 62(5), 900\u2013913 (2013)","journal-title":"IEEE Trans. Comput."},{"key":"8_CR31","unstructured":"Russinoff, D., Kaufmann, M., Smith, E., Sumners, R.: Formal verification of floating-point RTL at AMD using the ACL2 theorem prover. In: Proceedings of the 17th IMACS World Congress on Scientific Computation, Applied Mathematics and Simulation, Paris, France (2005)"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"Reeber, E., Sawada, J.: Combining ACL2 and an automated verification tool to verify a multiplier. In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and Its Applications, pp. 63\u201370. ACM (2006)","DOI":"10.1145\/1217975.1217990"},{"key":"8_CR33","doi-asserted-by":"publisher","unstructured":"Sawada, J., Reeber, E.: ACL2SIX: a hint used to integrate a theorem prover and an automated verification tool. In: Formal Methods in Computer Aided Design, 2006. FMCAD \u201906, pp. 161\u2013170 (2006). doi:\n                    10.1109\/FMCAD.2006.3","DOI":"10.1109\/FMCAD.2006.3"},{"key":"8_CR34","doi-asserted-by":"crossref","unstructured":"Sawada, J., Gamboa, R.: Mechanical verification of a square root algorithm using Taylor\u2019s theorem. In: Formal Methods in Computer-Aided Design, pp. 274\u2013291. Springer (2002)","DOI":"10.1007\/3-540-36126-X_17"},{"key":"8_CR35","unstructured":"Sawada, J., Sandon, P., Paruthi, V., Baumgartner, J., Case, M., Mony, H.: Hybrid verification of a hardware modular reduction engine. In: Proceedings of the International Conference on Formal Methods in Computer-Aided Design, FMCAD Inc, Austin, TX, FMCAD \u201911, pp. 207\u2013214 (2011). \n                    http:\/\/dl.acm.org.ezproxy.lib.utexas.edu\/citation.cfm?id=2157654.2157686"},{"key":"8_CR36","doi-asserted-by":"publisher","unstructured":"O\u2019Leary, J.W., Russinoff, D.M.: Modeling algorithms in SystemC and ACL2. In: Verbeek, F., Schmaltz, J. (eds.) Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014, Open Publishing Association, Electronic Proceedings in Theoretical Computer Science, vol. 152, pp. 145\u2013162 (2014). doi:\n                    10.4204\/EPTCS.152.12","DOI":"10.4204\/EPTCS.152.12"},{"key":"8_CR37","doi-asserted-by":"publisher","unstructured":"Coglio, A.: Second-order functions and theorems in ACL2. In: Kaufmann, M., Rager, D.L. (eds.) Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015, Open Publishing Association, Electronic Proceedings in Theoretical Computer Science, vol. 192, pp. 17\u201333 (2015). doi:\n                    10.4204\/EPTCS.192.3","DOI":"10.4204\/EPTCS.192.3"},{"key":"8_CR38","doi-asserted-by":"publisher","unstructured":"Selfridge, S., Smith, E.W.: Polymorphic types in ACL2. In: Verbeek, F., Schmaltz, J., (eds.) Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014, Open Publishing Association, Electronic Proceedings in Theoretical Computer Science, vol. 152, pp. 49\u201359 (2014). doi:\n                    10.4204\/EPTCS.152.4","DOI":"10.4204\/EPTCS.152.4"},{"key":"8_CR39","doi-asserted-by":"crossref","unstructured":"Rager, D.L., Ebergen, J., Lee, A., Nadezhin, D., Selfridge, B., Chau, C.K.: A brief introduction to oracle\u2019s use of ACL2 in verifying floating-point and integer arithmetic. In: Kaufmann, M., Rager, D.L. (eds.) Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015, Open Publishing Association, Electronic Proceedings in Theoretical Computer Science, vol. 192 (2015)","DOI":"10.4204\/EPTCS.192.1"},{"key":"8_CR40","unstructured":"Greve, D.: Address enumeration and reasoning over linear address spaces. In: Fifth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2004) (2004)"},{"key":"8_CR41","unstructured":"Greve, D., Richards, R., Wilding, M.: A summary of intrinsic partitioning verification. In: 5th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2004), Austin, TX (2004)"},{"key":"8_CR42","doi-asserted-by":"publisher","unstructured":"Hardin, D.S., Smith, E.W., Young, W.D.: A robust machine code proof framework for highly secure applications. In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and Its Applications, pp. 11\u201320. ACM, New York, NY, USA, ACL2 \u201906 (2006). doi:\n                    10.1145\/1217975.1217978","DOI":"10.1145\/1217975.1217978"},{"key":"8_CR43","unstructured":"CLHS (Accessed: October, 2015) Common Lisp HyperSpec. \n                    http:\/\/www.lispworks.com\/reference\/HyperSpec\/index.html"},{"key":"8_CR44","unstructured":"ACL2 Feature: Guards (Accessed: October, 2015). See \n                    http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/manuals\/current\/manual\/?topic=ACL2____GUARD"},{"key":"8_CR45","doi-asserted-by":"crossref","unstructured":"Greve, D.A., Kaufmann, M., Manolios, P., Moore, J.S., Ray, S., Ruiz-Reina, J.-L., Sumners, R., Vroon, D., Wilding, M.: Efficient execution in an automated reasoning environment. J. Funct. Program. 18(1) (2008)","DOI":"10.1017\/S0956796807006338"},{"key":"8_CR46","unstructured":"System Class Integer (Accessed: October, 2015) CLHS, Common Lisp HyperSpec. \n                    http:\/\/www.lispworks.com\/documentation\/HyperSpec\/Body\/t_intege.htm"},{"key":"8_CR47","unstructured":"ACL2 Feature: Trust Tags (Accessed: October, 2015). See \n                    http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/manuals\/current\/manual\/?topic=ACL2____DEFTTAG"},{"key":"8_CR48","unstructured":"ACL2 Feature: Untouchable Functions (Accessed: October, 2015). See \n                    http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/manuals\/current\/manual\/?topic=ACL2____PUSH-UNTOUCHABLE"},{"key":"8_CR49","unstructured":"The CompCert Project (Accessed: October, 2015). The CompCert C Compiler. \n                    http:\/\/compcert.inria.fr\/compcert-C.html"},{"key":"8_CR50","unstructured":"Linux Memory Management (Accessed: October, 2015). Linux System Administrators Guide. \n                    http:\/\/www.tldp.org\/LDP\/sag\/html\/memory-management.html"},{"key":"8_CR51","unstructured":"McKusick, M.K., Neville-Neil, G.V., Watson, R.N.M.: Chapter 6: Memory Management. The Design and Implementation of the FreeBSD Operating System, Addison Wesley Professional (2014)"},{"key":"8_CR52","unstructured":"Kerrisk, M.: The Linux Programming Interface: A Linux and UNIX System Programming Handbook, 1st edn. No Starch Press, San Francisco (2010)"},{"key":"8_CR53","unstructured":"Windows Memory Management (Accessed: October, 2015.) Windows System Administrators Guide. \n                    http:\/\/msdn.microsoft.com\/en-us\/library\/windows\/desktop\/aa366779(v=vs.85).aspx"},{"key":"8_CR54","doi-asserted-by":"crossref","unstructured":"Yu, D., Shao, Z.: Verification of safety properties for concurrent assembly code. In: Proceedings of 2004 International Conference on Functional Programming (ICFP\u201904) (2004)","DOI":"10.1145\/1016850.1016875"},{"key":"8_CR55","doi-asserted-by":"publisher","unstructured":"Morrisett, G., Tan, G., Tassarotti, J., Tristan, J.-B., Gan, E.: RockSalt: better, faster, stronger SFI for the x86. In: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 395\u2013404. ACM, PLDI \u201912 (2012). doi:\n                    10.1145\/2254064.2254111","DOI":"10.1145\/2254064.2254111"},{"key":"8_CR56","unstructured":"Myreen, M.O.: Formal Verification of Machine-code Programs. PhD thesis, University of Cambridge, Computer Laboratory, Trinity College (2008). \n                    http:\/\/www.cl.cam.ac.uk\/~mom22\/thesis.pdf"},{"key":"8_CR57","unstructured":"Smith, E.W.: Axe, An Automated Formal Equivalence Checking Tool For Programs. PhD thesis, Department of Computer Science, Stanford University (2011)"},{"key":"8_CR58","unstructured":"Moore, J.S.: (Accessed: October, 2015) Codewalker. See \n                    https:\/\/github.com\/acl2\/acl2\/books\/projects\/codewalker"},{"key":"8_CR59","unstructured":"Myreen, M.O., Gordon, M.J.C., Slind, K.: Decompilation into logic - improved. In: Formal Methods in Computer-Aided Design (FMCAD), 2012, pp. 78\u201381 (2012). \n                    http:\/\/www.cs.utexas.edu\/~hunt\/FMCAD\/FMCAD12\/016.pdf"},{"key":"8_CR60","unstructured":"Bellard, F.: QEMU, a fast and portable dynamic translator. In: USENIX Annual Technical Conference, FREENIX Track, pp. 41\u201346 (2005)"},{"key":"8_CR61","unstructured":"Lawton, K.P.: Bochs: A Portable PC Emulator for Unix\/X. Linux J 1996(29es) (1996). \n                    http:\/\/dl.acm.org\/citation.cfm?id=326350.326357"},{"key":"8_CR62","unstructured":"Unicorn (Accessed: October, 2015) Unicorn: Slides from BlackHat USA 2015. \n                    http:\/\/www.unicorn-engine.org\/BHUSA2015-unicorn.pdf"},{"key":"8_CR63","unstructured":"AMD Manuals (Accessed: October, 2015.) AMD64 Architecture: Developer Guides, Manuals and ISA Documents. \n                    http:\/\/developer.amd.com\/resources\/documentation-articles\/developer-guides-manuals\/"},{"key":"8_CR64","unstructured":"Goel, S., Hunt Jr., W.A., Kaufmann, M.: Abstract stobjs and their application to ISA modeling. In: Proceedings of the ACL2 Workshop 2013, EPTCS 114, pp. 54\u201369 (2013). \n                    http:\/\/arxiv.org\/pdf\/1304.7858.pdf"},{"key":"8_CR65","doi-asserted-by":"publisher","unstructured":"Luk, C.-K., Cohn, R., Muth, R., Patil, H., Klauser, A., Lowney, G., Wallace, S., Reddi, V.J., Hazelwood, K.: Pin: Building Customized Program Analysis Tools with Dynamic Instrumentation. SIGPLAN Not 40(6), 190\u2013200 (2005). doi:\n                    10.1145\/1064978.1065034","DOI":"10.1145\/1064978.1065034"},{"key":"8_CR66","unstructured":"Kaufmann, M., Hunt Jr., W.A.: Towards a Formal Model of the x86 ISA. Technical report, Department of Computer Science, University of Texas at Austin, Technical Report TR-12-07 (May 2012). see \n                    http:\/\/apps.cs.utexas.edu\/tech_reports\/reports\/tr\/TR-2075.pdf"},{"key":"8_CR67","unstructured":"Moore, J.S.: (Accessed: October, 2015.) Mechanized Operational Semantics. Lectures in the Marktoberdorf Summer School (August 5-16, 2008). See \n                    http:\/\/www.cs.utexas.edu\/users\/moore\/publications\/talks\/marktoberdorf-08\/index.html"},{"key":"8_CR68","doi-asserted-by":"crossref","unstructured":"Boyer, R.S., Moore, J.S.: Single-threaded Objects in ACL2. In: Krishnamurthy, S., Ramakrishnan, C.R. (eds.) Practical Aspects of Declarative Languages (PADL), vol. 2257, pp. 9\u201327. Springer, LNCS (2002)","DOI":"10.1007\/3-540-45587-6_3"},{"key":"8_CR69","unstructured":"Hunt Jr., W.A., Kaufmann, M.: A formal model of a large memory that supports efficient execution. In: Proceedings of the 12th International Conference on Formal Methods in Computer-Aided Design (FMCAD\u00a02012, Cambrige, UK, October 22\u201325) (2012). \n                    http:\/\/www.cs.utexas.edu\/~hunt\/FMCAD\/FMCAD12\/014.pdf"},{"key":"8_CR70","unstructured":"ACL2 Feature: Abstract Stobjs (Accessed: October, 2015). \n                    http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/manuals\/current\/manual\/index.html?topic=ACL2____DEFABSSTOBJ"},{"key":"8_CR71","unstructured":"Kaufmann, M., Sumners, R.: Efficient rewriting of operations on finite structures in ACL2. In: ETAPS 2002: European joint conference on theory and practice of software. Satellite workshop, pp. 141\u2013150 (2002)"},{"key":"8_CR72","unstructured":"Greve, D.: Scalable normalization for heap manipulating functions. In: ACL2 Workshop 2007 (2007). \n                    http:\/\/www.cs.uwyo.edu\/~ruben\/acl2-07\/uploads\/Main\/017.pdf"},{"key":"8_CR73","unstructured":"Goel, S., Hunt Jr., W.A., Kaufmann, M., Ghosh, S.: Simulation and formal verification of x86 machine-code programs that make system calls. In: Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design (FMCAD\u201914), pp. 18:91\u201398 (2014). \n                    http:\/\/dl.acm.org\/citation.cfm?id=2682923.2682944"},{"key":"8_CR74","unstructured":"Bitops (Accessed: October, 2015) An ACL2 Library for Reasoning about Bit-Vector Arithmetic. See \n                    http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/manuals\/current\/manual\/?topic=ACL2____BITOPS"},{"key":"8_CR75","unstructured":"Rager D.L.: (Accessed: October, 2015.) Maintaining community [in] sanity with Jenkins and Github. ACL2 Workshop 2015, Rump Session Talk. See \n                    https:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/workshop-2015\/rump-session-abstracts.html#rager\n                    \n                   and \n                    http:\/\/leeroy.defthm.com\/"},{"key":"8_CR76","unstructured":"Matz, M., Hubicka, J., Jaeger, A., Mitchell, M.: Chapter 4: Object Files in System V Application Binary Interface. AMD64 Architecture Processor Supplement, Draft v0 99 (2005)"},{"key":"8_CR77","unstructured":"Mach-O File Format (Accessed: October, 2015.) OS X ABI Mach-O File Format Reference. Mac Developer Library. \n                    https:\/\/developer.apple.com\/library\/mac\/documentation\/DeveloperTools\/Conceptual\/MachORuntime\/index.html"},{"key":"8_CR78","doi-asserted-by":"publisher","unstructured":"Swords, S., Davis, J.: Bit-blasting ACL2 theorems. In: Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2011, Austin, Texas, USA, November 3\u20134, 2011, pp. 84\u2013102 (2011). doi:\n                    10.4204\/EPTCS.70.7","DOI":"10.4204\/EPTCS.70.7"},{"key":"8_CR79","unstructured":"Anderson, S.: (Accessed: 2015) Bit Twiddling Hacks. See \n                    http:\/\/graphics.stanford.edu\/~seander\/bithacks.html"},{"key":"8_CR80","doi-asserted-by":"publisher","unstructured":"Goel, S., Hunt Jr., W.A.: Automated code proofs on a formal model of the x86. In: Verified Software: Theories, Tools, Experiments (VSTTE\u201913). Lecture Notes in Computer Science, vol. 8164, pp. 222\u2013241. Springer, Berlin, Heidelberg (2014). doi:\n                    10.1007\/978-3-642-54108-7_12","DOI":"10.1007\/978-3-642-54108-7_12"},{"key":"8_CR81","doi-asserted-by":"publisher","unstructured":"Moore, J.S.: Stateman: using metafunctions to manage large terms representing machine states. In: Kaufmann, M., Rager, D.L. (eds.) Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015, Open Publishing Association, Electronic Proceedings in Theoretical Computer Science, vol. 192, pp. 93\u2013109 (2015). doi:\n                    10.4204\/EPTCS.192.8","DOI":"10.4204\/EPTCS.192.8"},{"key":"8_CR82","unstructured":"Turing, A.M.: Checking a Large Routine, pp. 67\u201369 (1949). \n                    http:\/\/www.turingarchive.org\/browse.php\/B\/8"},{"key":"8_CR83","unstructured":"Hunt Jr., W.A.: Microprocessor design verification. J. Autom. Reason. 5(4), 429\u2013460 (1989). \n                    http:\/\/www.cs.utexas.edu\/~boyer\/ftp\/cli-reports\/048.pdf"},{"key":"8_CR84","unstructured":"Moore, J.S.: Piton: A Mechanically Verified Assembly-Level Language. Automated Reasoning Series. Kluwer Academic Publishers (1996)"},{"issue":"4","key":"8_CR85","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/BF00243134","volume":"5","author":"William D Young","year":"1989","unstructured":"Young, William D.: A mechanically verified code generator. J. Autom. Reason. 5(4), 493\u2013518 (1989)","journal-title":"J. Autom. Reason."},{"key":"8_CR86","doi-asserted-by":"crossref","unstructured":"Boyer, R.S., Yu, Y.: Automated proofs of object code for a widely used microprocessor. J. ACM 43(1), 166\u2013192 (1996). \n                    http:\/\/dl.acm.org\/citation.cfm?id=227603","DOI":"10.1145\/227595.227603"},{"key":"8_CR87","unstructured":"Bryant, R.E., O\u2019Hallaron, D.R.: Chapter 4: Processor Architecture, of Computer Systems: A Programmer\u2019s Perspective. Prentice-Hall (2003)"},{"key":"8_CR88","unstructured":"Goel, S., Hunt Jr., W.A., Kaufmann, M., Krug, R.: (Accessed: 2015) y86 Specifications in the ACL2 Community Books. See \n                    https:\/\/github.com\/acl2\/acl2\/tree\/master\/books\/models\/y86"},{"key":"8_CR89","doi-asserted-by":"publisher","unstructured":"Greve, D.A.: Symbolic simulation of the JEM1 microprocessor. In: Gopalakrishnan, G., Windley, P., (eds.) Formal Methods in Computer-Aided Design. Lecture Notes in Computer Science, vol. 1522, pp. 321\u2013333. Springer, Berlin, Heidelberg (1998). doi:\n                    10.1007\/3-540-49519-3_21","DOI":"10.1007\/3-540-49519-3_21"},{"key":"8_CR90","doi-asserted-by":"crossref","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) 11th International Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence, vol. 607, pp. 748\u2013752. Springer, Saratoga, NY (1992)","DOI":"10.1007\/3-540-55602-8_217"},{"key":"8_CR91","doi-asserted-by":"crossref","unstructured":"Greve, D., Wilding, M., Hardin, D.: High-speed, analyzable simulators. In: Computer-Aided Reasoning, pp. 113\u2013135. Springer (2000)","DOI":"10.1007\/978-1-4757-3188-0_8"},{"issue":"3","key":"8_CR92","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1023\/A:1011217102270","volume":"18","author":"M Wilding","year":"2001","unstructured":"Wilding, M., Greve, D., Hardin, D.: Efficient simulation of formal processor models. Form. Methods Syst. Des. 18(3), 233\u2013248 (2001)","journal-title":"Form. Methods Syst. Des."},{"key":"8_CR93","doi-asserted-by":"crossref","unstructured":"Fox, A.: Formal specification and verification of ARM6. In: Theorem Proving in Higher Order Logics, pp. 25\u201340. Springer (2003)","DOI":"10.1007\/10930755_2"},{"key":"8_CR94","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 DAMP 2009: the 4th Workshop on Declarative Aspects of Multicore Programming, ACM, New York, NY, USA, 553091 (2009)"},{"key":"8_CR95","doi-asserted-by":"crossref","unstructured":"Sewell, P., Sarkar, S., Owens, S., Zappa Nardelli, F., Myreen, M.O.: x86-TSO: a rigorous and usable programmer\u2019s model for x86 multiprocessors. Commun. ACM 53(7), 89\u201397 (2010) (Research Highlights)","DOI":"10.1145\/1785414.1785443"},{"key":"8_CR96","doi-asserted-by":"crossref","unstructured":"Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In: Proceedings of TPHOLs 2009: Theorem Proving in Higher Order Logics, LNCS 5674, pp. 391\u2013407 (2009)","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"8_CR97","doi-asserted-by":"publisher","unstructured":"Sarkar, S., Sewell, P., Zappa Nardelli, F., Owens, S., Ridge, T., Braibant, T., Myreen, M., Alglave, J.: The semantics of x86-CC multiprocessor machine code. In: Proceedings of POPL 2009: the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, pp. 379\u2013391 (2009). doi:\n                    10.1145\/1594834.1480929","DOI":"10.1145\/1594834.1480929"},{"key":"8_CR98","unstructured":"Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993)"},{"key":"8_CR99","doi-asserted-by":"publisher","unstructured":"Fox, A., Myreen, M.O.: A trustworthy monadic formalization of the ARMv7 instruction set architecture. In: Kaufmann, M., Paulson, L.C., (eds.) Interactive Theorem Proving, Lecture Notes in Computer Science, vol. 6172, pp. 243\u2013258. Springer, Berlin (2010). doi:\n                    10.1007\/978-3-642-14052-5_18","DOI":"10.1007\/978-3-642-14052-5_18"},{"key":"8_CR100","doi-asserted-by":"publisher","unstructured":"Myreen, M.O., Gordon, M., Slind, K.: Machine-code verification for multiple architectures - an application of decompilation into logic. In: Formal Methods in Computer-Aided Design, 2008. FMCAD \u201908, pp. 1\u20138 (2008). doi:\n                    10.1109\/FMCAD.2008.ECP.24\n                    \n                  , \n                    http:\/\/www.cl.cam.ac.uk\/~mom22\/decomp.pdf","DOI":"10.1109\/FMCAD.2008.ECP.24"},{"key":"8_CR101","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., et al.: seL4: formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, pp. 207\u2013220. ACM (2009). \n                    http:\/\/www.sigops.org\/sosp\/sosp09\/papers\/klein-sosp09.pdf"},{"key":"8_CR102","unstructured":"sel4: General Dynamics C4 Systems (Accessed: October, 2015). \n                    http:\/\/sel4.systems\/"},{"key":"8_CR103","doi-asserted-by":"publisher","unstructured":"Morrisett, G.: Scalable formal machine models. In: Proceedings of the Second International Conference on Certified Programs and Proofs, pp. 1\u20133. Springer, Berlin, Heidelberg, CPP\u201912 (2012). doi\n                    10.1007\/978-3-642-35308-6_1","DOI":"10.1007\/978-3-642-35308-6_1"},{"key":"8_CR104","unstructured":"Coq Proof Assistant (Accessed: October, 2015). \n                    http:\/\/coq.inria.fr\/"},{"key":"8_CR105","unstructured":"Feng, X., Shao, Z., Guo, Y., Dong, Y.: Certifying low-level programs with hardware interrupts and preemptive threads. J. Autom. Reason. 42(2), 301\u2013347 (2009). \n                    http:\/\/flint.cs.yale.edu\/flint\/publications\/aimjar.pdf"},{"key":"8_CR106","doi-asserted-by":"publisher","unstructured":"Shao, Z.: Clean-slate development of certified OS kernels. In: Proceedings of the 2015 Workshop on Certified Programs and Proofs, pp. 95\u201396. ACM, New York, NY, USA, CPP \u201915 (2015). doi:\n                    10.1145\/2676724.2693180","DOI":"10.1145\/2676724.2693180"},{"key":"8_CR107","unstructured":"Fox, A.: Directions in ISA Specification. Interactive Theorem Proving (ITP), pp. 338\u2013344 (2012). \n                    https:\/\/www.cl.cam.ac.uk\/~acjf3\/papers\/itp12.pdf"},{"key":"8_CR108","unstructured":"Degenbaev, U.: Formal Specification of the x86 Instruction Set Architecture. PhD thesis, Universit\u00e4t des Saarlandes (2012). \n                    http:\/\/rg-master.cs.uni-sb.de\/publikationen\/UD11.pdf"},{"key":"8_CR109","unstructured":"Shi, X.: Certification of an instruction set simulator. PhD thesis, Universit\u00e9 de Grenoble (2013)"},{"key":"8_CR110","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009). \n                    http:\/\/gallium.inria.fr\/~xleroy\/publi\/compcert-CACM.pdf"},{"key":"8_CR111","unstructured":"Bj\u00f8rner, D.: A ProCoS project description. International Conference on AI and Robotics, North Holland (1989)"},{"key":"8_CR112","first-page":"128","volume":"50","author":"JP Bowen","year":"1993","unstructured":"Bowen, J.P.: A ProCoS II project description: ESPRIT Basic Research project 7071. Bull. Eur. Assoc. Theor. Comput. Sci. (EATCS) 50, 128\u2013137 (1993)","journal-title":"Bull. Eur. Assoc. Theor. Comput. Sci. (EATCS)"}],"container-title":["NASA Monographs in Systems and Software Engineering","Provably Correct Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-48628-4_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,30]],"date-time":"2020-01-30T10:59:03Z","timestamp":1580381943000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-48628-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319486277","9783319486284"],"references-count":112,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-48628-4_8","relation":{},"ISSN":["1860-0131","2197-6597"],"issn-type":[{"value":"1860-0131","type":"print"},{"value":"2197-6597","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"2 March 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}