References

  1. Supporting materials. To appear in ACL2 Community Books under directory workshops/2013/.
  2. David A. Greve, Matt Kaufmann, Panagiotis Manolios, J. Strother Moore, Sandip Ray, José-Luis Ruiz-Reina, R. O. B. Sumners, Daron Vroon & Matthew Wilding (2008): Efficient execution in an automated reasoning environment. J. Funct. Program. 18(1). Available at http://dx.doi.org/10.1017/S0956796807006338.
  3. J S. Moore: Mechanized Operational Semantics. See URL http://www.cs.utexas.edu/users/moore/publications/talks/marktoberdorf-08/index.html.
  4. Warren A. Hunt Jr. & Matt Kaufmann (2012): A formal model of a large memory that supports efficient execution.. In: FMCAD, pp. 60–67. Available at http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6462556.
  5. M. Kaufmann: Trusted Extension of ACL2 System Code: Towards an Open Architecture. Workshop on Trusted Extensions of Interactive Theorem Provers, Cambridge, UK, 2010. http://www.cs.utexas.edu/users/kaufmann/itp-trusted-extensions-aug-2010/.
  6. M. Kaufmann & R. Sumners: Efficient Rewriting of Data Structures in ACL2. In: Proceedings of 3rd International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2002).
  7. M. Kaufmann and J S. Moore: ACL2 documentation topic: DEFABSSTOBJ. See URL http://www.cs.utexas.edu/users/moore/acl2/current/DEFABSSTOBJ.html.
  8. M. Kaufmann and J S. Moore: Essay on the Correctness of Abstract Stobjs. Comment in ACL2 source file other-events.lisp; see URL http://www.cs.utexas.edu/users/moore/acl2/".
  9. R. E. Bryant and D. R. OHallaron: Computer Systems: A Programmers Perspective ISBN: 0136108040.
  10. R. S. Boyer and J S. Moore (2002): Single-threaded Objects in ACL2. In: Practical Aspects of Declarative Languages (PADL), LNCS 2257. Springer-Verlag, pp. 9–27. Available at http://dx.doi.org/10.1007/3-540-45587-6_3.
  11. S. Ray & J S. Moore (2004): Proof Styles in Operational Semantics. In: Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2004), LNCS 3312. Springer-Verlag, Austin, TX, pp. 67–81. Available at http://dx.doi.org/10.1007/978-3-540-30494-4_6.
  12. S. Goel and W. Hunt: Automated Code Proofs on a Formal Model of the X86. To appear in VSTTE 2013.
  13. S. Swords (2010): A Verified Framework for Symbolic Execution in the ACL2 Theorem Prover. Department of Computer Sciences, The University of Texas at Austin. Available at http://hdl.handle.net/2152/ETD-UT-2010-12-2210.
  14. S. O. Swords (2013). Personal Communication.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org