References

1. Andrew W. Appel (1998): SSA is Functional Programming. In: SIGPLAN Notices 33. ACM, pp. 17–20, doi:10.1145/278283.278285.
2. Robert S. Boyer & J Strother Moore (2002): Single-Threaded Objects in ACL2. PADL 2002, doi:10.1007/3-540-45587-6_3.
3. Cristian Cadar, Daniel Dunbar & Dawson Engler (2008): KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs. In: Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, OSDI'08. USENIX Association, pp. 209–224. Available at http://dl.acm.org/citation.cfm?id=1855741.1855756.
4. Ron Cytron, Jeanne Ferrante, Barry K. Rosen, Mark N. Wegman & F. Kenneth Zadeck (1991): Efficiently Computing Static Single Assignment Form and the Control Dependence Graph. In: TOPLAS 13. ACM, pp. 451–490, doi:10.1145/115372.115320.
5. Damien Doligez, Alain Frisch, Jacques Garrigue, Didier Remy & Jerome Vouillon (2014): The OCaml System Release 4.02 Documentation and Users Guide. http://caml.inria.fr/distrib/ocaml-4.02/ocaml-4.02-refman.pdf.
6. Stephan Falke, Deepak Kapur & Carsten Sinz (2011): Termination Analysis of C Programs Using Compiler Intermediate Languages. In: Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA '11), pp. 41–50, doi:10.4230/LIPIcs.RTA.2011.41.
7. Stephan Falke, Florian Merz & Carsten Sinz (2013): The Bounded Model Checker LLBMC (Tool Demonstration). In: Proceedings of the 28th International Conference on Automated Software Engineering (ASE '13).
8. Anthony Fox (2012): Directions in ISA Specification. In: ITP 2012, doi:10.1007/978-3-642-32347-8_23.
9. David S. Hardin, Jennifer A. Davis, David A. Greve & Jedidiah R. McClurg (2014): Development of a Translator from LLVM to ACL2. In: F. Verbeek & J. Schmaltz: Proceedings of the 12th International Workshop on the ACL2 Theorem Prover and its Applications 152. EPTCS, pp. 163 – 177, doi:10.4204/EPTCS.152.13.
10. David S. Hardin & Samuel S. Hardin (2013): ACL2 Meets the GPU: Formalizing a CUDA-based Parallelizable All-Pairs Shortest Path Algorithm in ACL2. In: R. Gamboa & J. Davis: Proceedings of the 11th International Workshop on the ACL2 Theorem Prover and its Applications 114. EPTCS, pp. 127 – 142, doi:10.4204/EPTCS.114.10.
11. David S. Hardin, Jedidiah R. McClurg & Jennifer A. Davis (2013): Creating Formally Verified Components for Layered Assurance with an LLVM-to-ACL2 Translator. In: Proceedings of the 2013 Layered Assurance Workshop. ACM.
12. Matt Kaufmann, Panagiotis Manolios & J Strother Moore (2000): Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, doi:10.1007/978-1-4757-3188-0.
13. Xavier Leroy (2009): Formal Verification of a Realistic Compiler. In: Communications of the ACM 52, pp. 107–115, doi:10.1145/1538788.1538814.
14. Tim Lindholm, Frank Yellin, Gilad Bracha & Alex Buckley: The Java Virtual Machine Specification, Java SE 8 Edition. https://docs.oracle.com/javase/specs/jvms/se8/jvms8.pdf.
15. LispWorks Ltd.: Common Lisp HyperSpec. http://www.lispworks.com/documentation/HyperSpec/Front/index.htm.
16. LLVM Project: The LLVM Compiler Infrastructure. http://llvm.org/.
17. J Strother Moore (1999): Proving Theorems about Java-like Byte Code. In: E.-R. Olderog & B. Steffen: Correct System Design — Recent Insights and Advances, Lecture Notes in Computer Science 1710. Springer-Verlag, pp. 139–162, doi:10.1007/3-540-48092-7_7.
18. J Strother Moore (2014): Codewalker source code. Standard ACL2 distribution at http://www.cs.utexas.edu/users/moore/acl2.
19. Magnus O. Myreen, Michael J. C. Gordon & Konrad L. Slind (2012): Decompilation into Logic — Improved. In: FMCAD'12. ACM/IEEE.
20. Eric Smith (2011): Axe: An Automated Formal Equivalence Checking Tool for Programs. Stanford University.
21. The Coq Development Team (2015): The Coq Proof Assistant Reference Manual, Version 8.4pl6. https://coq.inria.fr/distrib/current/files/Reference-Manual.pdf.
22. Jules Villard (2013): Here be wyverns! Verifying LLVM bitcode with llStar. Unpublished manuscript at http://www.doc.ic.ac.uk/~jvillar1/pub/llstar-draft-oct13.pdf.
23. Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin & Steve Zdancewic (2012): Formalizing the LLVM Intermediate Representation for Verified Program Transformations. In: POPL'12. ACM, doi:10.1145/2103621.2103709.

Comments and questions to: eptcs@eptcs.org

For website issues: webmaster@eptcs.org