References

  1. 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.
  2. M. Kaufmann, P. Manolios & J S. Moore (2000): Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Press, Boston, MA..
  3. 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.
  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.
  5. M. Kaufmann & J S. Moore (2015): Well-Formedness Guarantees for ACL2 Metafunctions and Clause Processors. In: (submitted for publication).
  6. 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.
  7. 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.
  8. Magnus O. Myreen (2009): Formal verification of machine-code programs. University of Cambridge.
  9. 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.
  10. 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.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org