@inproceedings(99-aagaard-param, author = "Mark D. Aagaard and Robert B. Jones and Carl-Johan H. Seger", year = "1999", title = "Formal verification using parametric representations of {Boolean} constraints", booktitle = "DAC '99", publisher = "IEEE", pages = "402--407", doi = "10.1145/309847.309968", ) @misc(11-anderson-bit-hacks, author = "Sean Eron Anderson", title = "Bit Twiddling Hacks", howpublished = "\url {http://graphics.stanford.edu/ seander/bithacks.html}", note = "Accessed June, 2011", ) @inproceedings(11-armand-sat, author = "Micha\"{e}l Armand and Germain Faure and Benjamin Gr\'{e}goire and Chantal Keller and Laurent Th\'{e}ry and Benjamin Werner", year = "2011", title = "Verifying {SAT} and {SMT} in {Coq} for a fully automated decision procedure", booktitle = "PSATTT '11", ) @inproceedings(06-boyer-acl2h, author = "Robert S. Boyer and Warren A. {Hunt, Jr.}", year = "2006", title = "Function Memoization and Unique Object Representation for {ACL2} Functions", booktitle = "ACL2 '06", publisher = "ACM", pages = "81--89", doi = "10.1145/1217975.1217992", ) @inproceedings(09-boyer-g, author = "Robert S. Boyer and Warren A. {Hunt, Jr.}", year = "2009", title = "Symbolic Simulation in {ACL2}", booktitle = "ACL2 '09", publisher = "ACM", pages = "20--24", doi = "10.1145/1637837.1637840", ) @inproceedings(98-chen-adders, author = "{Yirng-An} Chen and Randal E. Bryant", year = "1998", title = "Verification of floating-point adders", booktitle = "CAV '98", series = "LNCS", volume = "1427", publisher = "Springer", pages = "488--499", doi = "10.1007/BFb0028769", ) @inproceedings(10-darbari-sat, author = "Ashish Darbari and Bernd Fischer and Jo$\mathaccent "707E\relax {\textrm {a}}$o Marques-Silva", year = "2010", title = "Industrial-Strength Certified {SAT} Solving through Verified {SAT} Proof Checking", booktitle = "ICTAC '10", series = "LNCS", volume = "6255", publisher = "Springer", pages = "260--274", doi = "10.1007/978-3-642-14808-8\_18", ) @inproceedings(06-davis-input, author = "Jared Davis", year = "2006", title = "Reasoning about File Input in {ACL2}", booktitle = "ACL2 '06", publisher = "ACM", pages = "117--126", doi = "10.1145/1217975.1218000", ) @inproceedings(11-fox-blasting, author = "Anthony Fox", year = "2011", title = "{LCF}-Style Bit-Blasting in {HOL4}", booktitle = "ITP '11", series = "LNCS", publisher = "Springer", pages = "357--362", doi = "10.1007/978-3-642-22863-6\_26", ) @inproceedings(09-hunt-fadd, author = "Warren A. {Hunt, Jr.} and Sol Swords", year = "2009", title = "{Centaur} {Technology} Media Unit Verification", booktitle = "CAV '09", series = "LNCS", volume = "5643", publisher = "Springer", pages = "353--367", doi = "10.1007/978-3-642-02658-4\_28", ) @incollection(10-hardin-centaur, author = "Warren A. {Hunt, Jr.} and Sol Swords and Jared Davis and Anna Slobodov\'{a}", year = "2010", title = "Use of Formal Verification at {Centaur} {Technology}", editor = "David Hardin", booktitle = "Design and Verification of Microprocessor Systems for High-Assurance Applications", publisher = "Springer", pages = "65--88", ) @book(00-kaufmann-car, author = "Matt Kaufmann and Panagiotis Manolios and J Strother Moore", year = "2000", title = "Computer-Aided Reasoning: An Approach", publisher = "Kluwer Academic Publishers", ) @article(06-manolios-pipeline, author = "Panagiotis Manolios and Sudarshan K. Srinivasan", year = "2006", title = "A Framework for Verifying Bit-Level Pipelined Machines Based on Automated Deduction and Decision Procedures", journal = "Journal of Automated Reasoning", volume = "37", number = "1-2", pages = "93--116", doi = "10.1007/s10817-006-9035-0", ) @article(60-mccarthy-recursive, author = "John {McCarthy}", year = "1960", title = "Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part 1", journal = "Communications of the {ACM}", volume = "3", number = "4", pages = "184--195", doi = "10.1145/367177.367199", ) @inproceedings(06-reeber-sulfa, author = "Erik Reeber and Warren A. {Hunt, Jr.}", year = "2006", title = "A {SAT}-Based Decision Procedure for the Subclass of Unrollable List Functions in {ACL2} {(SULFA)}.", booktitle = "IJCAR '06", series = "LNCS", volume = "4130", publisher = "Springer", pages = "453--467", doi = "10.1007/11814771\_38", ) @phdthesis(07-reeber-dissertation, author = "Erik Henry Reeber", year = "2007", title = "Combining Advanced Formal Hardware Verification Techniques", school = "University of Texas at Austin", note = "\url {http://hdl.handle.net/2152/3662}", ) @inproceedings(11-slobodova-framework, author = "Anna Slobodov\'{a} and Jared Davis and Sol Swords and Warren A. {Hunt, Jr.}", year = "2011", title = "A Flexible Formal Verification Framework for Industrial Scale Validation", booktitle = "Memocode '11", publisher = "IEEE", pages = "89--97", doi = "10.1109/MEMCOD.2011.5970515", ) @phdthesis(07-srinivasan-dissertation, author = "Sundarshan Kumar Srinivasan", year = "2007", title = "Efficient Verification of Bit-Level Pipelined Machines Using Refinement", school = "Georgia Institute of Technology", note = "\url {http://hdl.handle.net/1853/19815}", ) @incollection(10-swords-bddify, author = "Sol Swords and Warren A. {Hunt, Jr.}", year = "2010", title = "A Mechanically Verified {AIG to BDD} Conversion Algorithm", booktitle = "ITP '10", series = "LNCS", volume = "6172", publisher = "Springer", pages = "435--449", doi = "10.1007/978-3-642-14052-5\_30", ) @phdthesis(10-swords-dissertation, author = "Sol Otis Swords", year = "2010", title = "A Verified Framework for Symbolic Execution in the {ACL2} Theorem Prover", school = "University of Texas at Austin", note = "\url {http://hdl.handle.net/2152/ETD-UT-2010-12-2210}", ) @article(09-weber-sat, author = "Tjark Weber and Hasan Amjad", year = "2009", title = "Efficiently Checking Propositional Refutations in {HOL} Theorem Provers", journal = "Journal of Applied Logic", volume = "7", number = "1", pages = "26--40", doi = "10.1016/j.jal.2007.07.003", )