paper.bib

@misc{acl2:home,
 author       = "{Matt Kaufmann and J S. Moore}",
 title        = "{ACL2} home page",
 key        = "{ACL2} home page",
 note         = "(see URL \url{http://www.cs.utexas.edu/users/moore/acl2})",
 year       = "Accessed: 2016"
}


@misc{centaur,
 key="{Centaur Technology}",
 howpublished="{\url{http://www.centtech.com}.}",
 year={Accessed: 2016}
 }

@misc{centaur-fv,
 key="FV Group at Centaur",
 howpublished="{\url{http://fv.centtech.com}.}",
 year={Accessed: 2016}
 }

@incollection{centaur-microcode,
year={2014},
isbn={978-3-319-08969-0},
booktitle={Interactive Theorem Proving},
volume={8558},
series={Lecture Notes in Computer Science},
editor={Klein, Gerwin and Gamboa, Ruben},
doi={10.1007/978-3-319-08970-6\_1},
title={Microcode Verification --- Another Piece of the Microprocessor Verification Puzzle},
publisher={Springer International Publishing},
author="{Jared Davis, Anna Slobodova, Sol Swords}",
pages={1-16},
language={English}
}

@article{trusted-cl-proc,
title = "{Integrating External Deduction Tools with ACL2}",
journal = "Journal of Applied Logic",
volume = "7",
number = "1",
pages = "3 - 25",
year = "2009",
note = "Special Issue: Empirically Successful Computerized Reasoning ",
issn = "1570-8683",
doi = {10.1016/j.jal.2007.07.002},
author = "{Matt Kaufmann, J S. Moore, Sandip Ray, and Erik Reeber}",
keywords = "Automated reasoning",
keywords = "Decision procedures",
keywords = "First-order logic",
keywords = "Interfaces",
keywords = "Theorem proving "
}

@inproceedings{bit-blasting-GL,
  author    = "{Sol Swords and Jared Davis}",
  title     = "{Bit-Blasting {ACL2} Theorems}",
  booktitle = {Proceedings 10th International Workshop on the {ACL2} Theorem Prover
               and its Applications, {ACL2} 2011, Austin, Texas, USA, November 3-4,
               2011.},
  pages     = {84--102},
  year      = {2011},
  doi       = {10.4204/EPTCS.70.7},
  timestamp = {Mon, 28 Oct 2013 16:56:55 +0100},
}

@PhdThesis{gl-diss,
  author  = "{Sol Swords}",
  title   = "{A Verified Framework for Symbolic Execution in the ACL2 Theorem Prover}",
  school  = "{Department of Computer Sciences,
             The University of Texas at Austin}",
  year    = "2010",
  url = {http://hdl.handle.net/2152/ETD-UT-2010-12-2210}
}

@Incollection{emod-hardin,
  author     = "{Warren A. Hunt, Jr., Sol Swords, Jared Davis, and Anna Slobodova}",
  title      = "{Use of Formal Verification at Centaur Technology}",
  booktitle  = "{Design and Verification of Microprocessor Systems for High-Assurance Applications}",
  editor    = "D. S. Hardin",
  pages     = "65--88",
  publisher = "Springer",
  year      = "2010",
  doi       = {10.1007/978-1-4419-1539-9\_3},
  url={https://www.cs.utexas.edu/~jared/publications/2010-hardin-centaur.pdf}
}

@inproceedings{centaur-framework,
author="{Anna Slobodova, Jared Davis, Sol Swords, and Warren A. Hunt, Jr.}",
booktitle="{9th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE), 2011}",
title="{A Flexible Formal Verification Framework for Industrial Scale Validation}",
year={2011},
month={July},
pages={89-97},
keywords={CAD;formal verification;integrated circuit design;microprocessor chips;production engineering computing;semiconductor device manufacture;CAD tools;CAD vendors;FV tools;design flows;formal verification framework;industrial scale validation;microprocessor companies;microprocessor design;Boolean functions;Clocks;Companies;Data structures;Hardware design languages;Integrated circuit modeling;Wires},
doi={10.1109/MEMCOD.2011.5970515},}

@unpublished{defattach,
author="{Matt Kaufmann}",
title="{Trusted Extension of ACL2 System Code: Towards an Open Architecture}",
note="See \url{http://www.cs. utexas.edu/users/kaufmann/itp-trusted-extensions-aug-2010/}",
year="August 11-12, 2010",
series="Workshop on Trusted Extensions of Interactive Theorem Provers, Cambridge, UK"
}

@inproceedings{meta-05,
author="Hunt, Jr., W. A. and M.~Kaufmann and R.~B.~Krug and J S.~Moore
        and E.~W.~Smith",
title="Meta Reasoning in {ACL2}",
doi={10.1007/11541868\_11},
booktitle="18th International Conference on Theorem
           Proving in Higher Order Logics: {TPHOLs} 2005",
editor="J.~Hurd and T.~Melham",
publisher = {Springer},
series    = {Lecture Notes in Computer Science},
volume    = {3603},
pages     = {163--178},
year      = {2005}}

@Incollection{meta,
 author="R. S. Boyer and J S. Moore",
 title="Metafunctions: Proving Them Correct and Using Them Efficiently
        as New Proof Procedures",
 booktitle="The Correctness Problem in Computer Science",
 publisher="Academic Press, London",
 editors="R. S. Boyer and J S. Moore",
 year="1981"}

@techreport{davis09,
 author="J. Davis",
 title="A Self-Verifying Theorem Prover",
 institution="University of Texas at Austin",
 year="2009",
 note="(see \url{http://www.cs.utexas.edu/~jared/milawa/Web/})"}

@inproceedings{greve06,
 author = {Greve, David},
 title = {Parameterized Congruences in ACL2},
 booktitle = {Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and Its Applications},
 series = {ACL2 '06},
 year = {2006},
 isbn = {0-9788493-0-2},
 location = {Seattle, Washington, USA},
 pages = {28--34},
 numpages = {7},
 doi = {10.1145/1217975.1217981},
 acmid = {1217981},
 publisher = {ACM},
 address = {New York, NY, USA},
}

@misc{acl2:doc,
 author       = "{ACL2 Community}",
 title        = "{ACL2+Books} Documentation",
 key        = "{ACL2+Books} Documentation",
 url        = {http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html},
 year = "accessed January, 2017"
}

@misc{acl2-github,
 author       = "{ACL2 Community}",
 title        = "{ACL2} System and Libraries on {GitHub}",
 howpublished="{\url{https://github.com/acl2/acl2/tree/master/books/}}",
 year={Accessed: 2016}
}