S. Goel, W.A. Hunt & M. Kaufmann (2014):
Simulation and Formal Verification of x86 Machine-Code Programs that make System Calls.
In: K. Claessen & V. Kuncak: FMCAD'14: Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD14/proceedings/final.pdf.
EPFL, Switzerland,
pp. 91–98,
doi:10.1109/FMCAD.2014.6987600.
M. Kaufmann, P. Manolios & J S. Moore (2000):
Computer-Aided Reasoning: ACL2 Case Studies.
Kluwer Academic Press,
Boston, MA..
M. Kaufmann, P. Manolios & J S. Moore (2000):
Computer-Aided Reasoning: An Approach.
Kluwer Academic Press,
Boston, MA.,
doi:10.1007/978-1-4615-4449-4.
M. Kaufmann & J S. Moore (2014):
The ACL2 Home Page.
In: http://www.cs.utexas.edu/users/moore/acl2/.
Dept. of Computer Sciences, University of Texas at Austin.
M. Kaufmann & J S. Moore (2015):
Well-Formedness Guarantees for ACL2 Metafunctions and Clause Processors.
In: (submitted for publication).
H. Liu & J S. Moore (2004):
Java Program Verification via a JVM Deep Embedding in ACL2.
In: K. Slind, A. Bunker & G. Gopalakrishnan: 17th International Conference on Theorem Proving in Higher Order Logics: TPHOLs 2004,
Lecture Notes in Computer Science 3223.
Springer,
pp. 184–200,
doi:10.1007/978-3-540-30142-4_14.
J S. Moore & M. Martinez (2009):
A Mechanically Checked Proof of the Correctness of the Boyer-Moore Fast String Searching Algorithm.
In: Engineering Methods and Tools for Software Safety and Security (Proceedings of the Martoberdorf Summer School, 2008).
IOS Press,
pp. 267–284,
doi:10.3233/978-1-58603-976-9-267.
Magnus O. Myreen (2009):
Formal verification of machine-code programs.
University of Cambridge.
Magnus O. Myreen, Konrad Slind & Michael J. C. Gordon (2012):
Decompilation into Logic — Improved.
In: Formal Methods in Computer-Aided Design (FMCAD), 2012,
pp. 78–81.
E. Toibazarov (2013):
An ACL2 Proof of the Correctness of the Preprocessing for a Variant of the Boyer-Moore Fast String Searching Algorithm.
Honors Thesis.
Computer Science Dept., University of Texas at Austin.
See http://www.cs.utexas.edu/users/moore/publications/toibazarov-thesis.pdf.