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