@misc(absstobj-support,
 title        = "{Supporting materials}",
 note         = "{To appear in {ACL2} Community Books under directory {\tt workshops/2013/}}",
)
@article(defexec,
 author       = "David~A. Greve and Matt Kaufmann and Panagiotis Manolios and J.~Strother Moore and Sandip Ray and Jos{\'e}-Luis Ruiz-Reina and R.~O.~B. Sumners and Daron Vroon and Matthew Wilding",
 year         = "2008",
 title        = "Efficient execution in an automated reasoning environment",
 journal      = "J. Funct. Program.",
 volume       = "18",
 number       = "1",
 url          = "http://dx.doi.org/10.1017/S0956796807006338",
)
@misc(mechanized-op-semantics,
 author       = "{J S. Moore}",
 title        = "{Mechanized Operational Semantics}",
 note         = "See URL \url {http://www.cs.utexas.edu/users/moore/publications/talks/marktoberdorf-08/index.html}",
)
@inproceedings(hunt-kaufmann-fmcad-2012,
 author       = "Warren A.~Hunt Jr. and Matt Kaufmann",
 year         = "2012",
 title        = "A formal model of a large memory that supports efficient execution.",
 booktitle    = "FMCAD",
 pages        = "60--67",
 url          = "http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6462556",
)
@misc(defattach-workshop,
 author       = "M.~Kaufmann",
 title        = "Trusted Extension of {ACL2} System Code: Towards an Open Architecture",
 note         = "Workshop on Trusted Extensions of Interactive Theorem Provers, Cambridge, UK, 2010. \url {http://www.cs.utexas.edu/users/kaufmann/itp-trusted-extensions-aug-2010/}",
)
@inproceedings(Kaufmann02efficientrewriting,
 author       = "M.~Kaufmann and R.~Sumners",
 title        = "{Efficient Rewriting of Data Structures in ACL2}",
 booktitle    = "{Proceedings of $3$rd International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2002)}",
)
@misc(defabsstobj-doc,
 author       = "{M. Kaufmann and J S. Moore}",
 title        = "{ACL2} documentation topic: {DEFABSSTOBJ}",
 note         = "See URL \url {http://www.cs.utexas.edu/users/moore/acl2/current/DEFABSSTOBJ.html}",
)
@misc(essay-absstobjs,
 author       = "{M. Kaufmann and J S. Moore}",
 title        = "{Essay on the Correctness of Abstract Stobjs}",
 note         = "Comment in {ACL2} source file {\tt other-events.lisp}; see URL \url {http://www.cs.utexas.edu/users/moore/acl2/}"",
)
@article(bryant2001computer,
 author       = "{R. E. Bryant and D. R. O\IeC {\textquoteright }Hallaron}",
 title        = "{Computer Systems: A Programmer\IeC {\textquoteright }s Perspective}",
 number       = "{ISBN: 0136108040}",
)
@inproceedings(stobjs,
 author       = "{R. S. Boyer and J S. Moore}",
 year         = "2002",
 title        = "{Single-threaded Objects in ACL2}",
 booktitle    = "{Practical Aspects of Declarative Languages (PADL)}",
 series       = "LNCS",
 volume       = "2257",
 publisher    = "Springer-Verlag",
 pages        = "9--27",
 url          = "http://dx.doi.org/10.1007/3-540-45587-6_3",
)
@inproceedings(raymoore,
 author       = "S.~Ray and J~S. Moore",
 year         = "2004",
 title        = "{Proof Styles in Operational Semantics}",
 booktitle    = "{Proceedings of the $5$th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2004)}",
 series       = "{LNCS}",
 volume       = "3312",
 publisher    = "{Springer-Verlag}",
 address      = "{Austin, TX}",
 pages        = "67--81",
 url          = "http://dx.doi.org/10.1007/978-3-540-30494-4_6",
)
@inproceedings(goel-hunt-popcount,
 author       = "{S. Goel and W. Hunt}",
 title        = "{Automated Code Proofs on a Formal Model of the X86}",
 note         = "{To appear in VSTTE 2013}",
)
@phdthesis(swords2011verified,
 author       = "S.~Swords",
 year         = "2010",
 title        = "A Verified Framework for Symbolic Execution in the {ACL2} Theorem Prover",
 school       = "{Department of Computer Sciences, The University of Texas at Austin}",
 url          = "http://hdl.handle.net/2152/ETD-UT-2010-12-2210",
)
@misc(sswords,
 author       = "S.~O. Swords",
 year         = "2013",
 note         = "{Personal Communication}",
)