Supporting materials.
To appear in ACL2 Community Books under directory workshops/2013/.
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.
J S. Moore:
Mechanized Operational Semantics.
See URL http://www.cs.utexas.edu/users/moore/publications/talks/marktoberdorf-08/index.html.
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/.
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).
M. Kaufmann and J S. Moore:
ACL2 documentation topic: DEFABSSTOBJ.
See URL http://www.cs.utexas.edu/users/moore/acl2/current/DEFABSSTOBJ.html.
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/".
R. E. Bryant and D. R. OHallaron:
Computer Systems: A Programmers Perspective ISBN: 0136108040.
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.
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.
S. Goel and W. Hunt:
Automated Code Proofs on a Formal Model of the X86.
To appear in VSTTE 2013.
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.