References

  1. ACL2 Theorem Prover and Community Books: User Manual. Online; accessed: September 2018. http://www.cs.utexas.edu/~moore/acl2/manuals/current/manual.
  2. ACL2 Books: Codewalker. Online; accessed: September 2018. https://github.com/acl2/acl2/tree/master/books/projects/codewalker.
  3. ACL2 Books: rtl/rel11 - A Formal Theory of Register-Transfer Logic and Computer Arithmetic. Online; accessed: September 2018. https://github.com/acl2/acl2/tree/master/books/rtl/rel11.
  4. ACL2 Books: y86 Specifications. Online; accessed: September 2018. https://github.com/acl2/acl2/tree/master/books/models/y86.
  5. APT (Automated Program Transformations): Web page. Online; accessed: September 2018. http://www.kestrel.edu/home/projects/apt.
  6. Christoph Baumann (2008): Formal Specification of the x86 Floating-Point Instruction Set. Universität des Saarlandes. Online; accessed: September 2018. http://www-wjp.cs.uni-saarland.de/publikationen/Ba08.pdf.
  7. Alessandro Coglio (2014): Pop-Refinement. Archive of Formal Proofs. Formal proof development. http://afp.sf.net/entries/Pop_Refinement.shtml.
  8. Alessandro Coglio, Matt Kaufmann & Eric Smith (2017): A Versatile, Sound Tool for Simplifying Definitions. In: Proc. 14th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2017), pp. 61–77, doi:10.4204/EPTCS.249.5.
  9. Ulan Degenbaev (2012): Formal Specification of the x86 Instruction Set Architecture. Universität des Saarlandes. Online; accessed: September 2018. http://rg-master.cs.uni-sb.de/publikationen/UD11.pdf.
  10. Anthony Fox & Magnus O. Myreen (2010): A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture. In: Matt Kaufmann and Lawrence C. Paulson: Interactive Theorem Proving, Lecture Notes in Computer Science 6172. Springer Berlin Heidelberg, pp. 243–258, doi:10.1007/978-3-642-14052-5_18.
  11. Shilpi Goel (2016): Formal Verification of Application and System Programs Based on a Validated x86 ISA Model. Department of Computer Science, The University of Texas at Austin. Online; accessed: September 2018. http://hdl.handle.net/2152/46437.
  12. Shilpi Goel (2017): The x86isa Books: Features, Usage, and Future Plans. In: Proc. 14th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2-2017), pp. 1–17, doi:10.4204/EPTCS.249.1.
  13. Shilpi Goel, Warren A. Hunt Jr. & Matt Kaufmann (2013): Abstract Stobjs and Their Application to ISA Modeling. In: Proc. International Workshop on the ACL2 Theorem Prover and its Applications (ACL2-2013), pp. 54–69, doi:10.4204/EPTCS.114.5.
  14. Shilpi Goel, Warren A. Hunt, Jr. & Matt Kaufmann (2017): Engineering a Formal, Executable x86 ISA Simulator for Software Verification. In: Provably Correct Systems. Springer International Publishing, Cham, pp. 173–209, doi:10.1007/978-3-319-48628-4_8. Editors: Mike Hinchey, Jonathan P. Bowen, and Ernst-Rüdiger.
  15. Intel Corporation: Intel 64 and IA-32 Architectures Software Developer's Manual. Online; accessed: September 2018. Order Number: 325462-067US. (May, 2018). http://www.intel.com/content/www/us/en/processors/architectures-software-developermanuals.html.
  16. John Leyden (2017): 64-bit malware threat may be itty-bitty now, but it's only set to grow. The Register. Online; accessed: September 2018. https://www.theregister.co.uk/2017/05/24/64bit_malware.
  17. Hanbing Liu & J S. Moore (2004): Java program verification via a JVM deep embedding in ACL2. In: International Conference on Theorem Proving in Higher Order Logics. Springer, pp. 184–200, doi:10.1007/978-3-540-30142-4_14.
  18. John McCarthy (1964): A Formal Description of a Subset of Algol. In: T. B. Steel: Formal Language Description Languages for Computer Programming, North Holland, 1966, pp. 1–12.
  19. J S. Moore: Mechanized Operational Semantics. Online; accessed: September 2018. Lectures in the Marktoberdorf Summer School (August 5-16, 2008). http://www.cs.utexas.edu/users/moore/publications/talks/marktoberdorf-08/index.html.
  20. Greg Morrisett, Gang Tan, Joseph Tassarotti, Jean-Baptiste Tristan & Edward Gan (2012): RockSalt: Better, Faster, Stronger SFI for the x86. In: Proc. of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '12. ACM, pp. 395–404, doi:10.1145/2254064.2254111.
  21. Michael Norrish (1998): C formalised in HOL. University of Cambridge. Online; accessed: September 2018. https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-453.pdf.
  22. Alastair Reid (2016): Trustworthy specifications of ARM v8-A and v8-M System level architecture. In: 2016 Formal Methods in Computer-Aided Design (FMCAD), pp. 161–168, doi:10.1109/FMCAD.2016.7886675.
  23. Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge, Thomas Braibant, Magnus Myreen & Jade Alglave (2009): The Semantics of x86-CC Multiprocessor Machine Code. In: Proc. 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 379–391, doi:10.1145/1594834.1480929.
  24. Jun Sawada & Warren A. Hunt, Jr. (2002): Verification of FM9801: An Out-of-Order Microprocessor Model with Speculative Execution, Exceptions, and Program-Modifying Capability. Formal Methods in Systems Design 20(2), pp. 187–222, doi:10.1023/A:1014122630277.
  25. Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli & Magnus O. Myreen (2010): x86-TSO: A Rigorous and Usable Programmer's Model for x86 Multiprocessors. Communications of the ACM 53(7), pp. 89–97, doi:10.1145/1785414.1785443.
  26. Sol Swords (2010): A Verified Framework for Symbolic Execution in the ACL2 Theorem Prover. Department of Computer Science, The University of Texas at Austin. Online; accessed: September 2018. http://hdl.handle.net/2152/ETD-UT-2010-12-2210.
  27. Sol Swords & Jared Davis (2011): Bit-Blasting ACL2 Theorems. In: Proc. 10th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2-2011), pp. 84–102, doi:10.4204/EPTCS.70.7.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org