@book(appel:prog-logic,
 author       = {Andrew W. Appel},
 year         = {2014},
 title        = {Program Logics for Certified Compilers},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9781107256552},
)
@inproceedings(Hatcliff2011,
 author       = {Jason Belt and John Hatcliff and Robby and Patrice Chalin and David S. Hardin and Xianghua Deng},
 year         = {2011},
 title        = {Bakar Kiasan: Flexible Contract Checking for Critical Systems using Symbolic Execution},
 booktitle    = {Proceedings of the Third NASA Formal Methods Symposium (NFM 2011)},
 pages        = {58 -- 72},
 doi          = {10.1007/978-3-642-20398-5\_6},
)
@inproceedings(stobj,
 author       = {Robert S. Boyer and J Strother Moore},
 year         = {2002},
 title        = {Single-Threaded Objects in {ACL2}},
 booktitle    = {Practical Aspects of Declarative Languages, 4th International Symposium, {PADL} 2002},
 series       = {LNCS},
 volume       = {2257},
 publisher    = {Springer},
 pages        = {9--27},
 doi          = {10.1007/3-540-45587-6_3},
)
@inproceedings(bedrock,
 author       = {Adam Chlipala},
 year         = {2013},
 title        = {The {B}edrock Structured Programming System: Combining Generative Metaprogramming and Hoare Logic in an Extensible Program Verifier},
 booktitle    = {Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming},
 series       = {ICFP '13},
 publisher    = {ACM Press},
 pages        = {391--402},
 doi          = {10.1145/2500365.2500592},
)
@inproceedings(why3,
 author       = {Jean-Christophe Filli\^atre and Andrei Paskevich},
 year         = {2013},
 title        = {Why3 --- Where Programs Meet Provers},
 editor       = {Matthias Felleisen and Philippa Gardner},
 booktitle    = {Proceedings of the 22nd European Symposium on Programming},
 series       = {LNCS},
 volume       = {7792},
 publisher    = {Springer},
 pages        = {125--128},
 doi          = {10.1007/978-3-642-37036-6_8},
)
@inproceedings(auto-corres,
 author       = {David Greenaway and Japheth Lim and June Andronick and Gerwin Klein},
 year         = {2014},
 title        = {Don't Sweat the Small Stuff: Formal Verification of {C} Code Without the Pain},
 booktitle    = {Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation},
 series       = {PLDI '14},
 publisher    = {ACM Press},
 pages        = {429--439},
 doi          = {10.1145/2594291.2594296},
)
@book(Hardin2010,
 editor       = {David S. Hardin},
 year         = {2010},
 title        = {Design and Verification of Microprocessor Systems for High-Assurance Applications},
 publisher    = {Springer},
 doi          = {10.1007/978-1-4419-1539-9},
)
@inproceedings(Hardin2009a,
 author       = {David S. Hardin and Samuel S. Hardin},
 year         = {2009},
 title        = {Efficient, Formally Verifiable Data Structures using {ACL2} Single-Threaded Objects for High-Assurance Systems},
 editor       = {S. Ray and D. Russinoff},
 booktitle    = {Proceedings of the Eighth International Workshop on the {ACL2} Theorem Prover and its Applications},
 publisher    = {ACM Press},
 pages        = {100 -- 105},
 doi          = {10.1145/1637837.1637853},
)
@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(Hardin2009b,
 author       = {David S. Hardin and T. Douglas Hiratzka and D. Randolph Johnson and Lucas G. Wagner and Michael W. Whalen},
 year         = {2009},
 title        = {Development of Security Software: A High Assurance Methodology},
 editor       = {K. Breitman and A. Cavalcanti},
 booktitle    = {Proceedings of the 11th International Conference on Formal Engineering Methods: Formal Methods and Software Engineering (ICFEM'09)},
 publisher    = {Springer},
 pages        = {266 -- 285},
 doi          = {10.1007/978-3-642-10373-5_14},
)
@inproceedings(GuardolVHDL,
 author       = {David S. Hardin and Konrad L. Slind and Mark A. Bortz and James Potts and Scott Owens},
 year         = {2016},
 title        = {A High-Assurance, High-Performance Hardware-Based Cross-Domain System},
 booktitle    = {Computer Safety, Reliability, and Security - 35th International Conference, {SAFECOMP} 2016},
 series       = {LNCS},
 volume       = {9922},
 publisher    = {Springer},
 pages        = {102--113},
 doi          = {10.1007/978-3-319-45477-1_9},
)
@inproceedings(guardol:tacas,
 author       = {David S. Hardin and Konrad L. Slind and Michael W. Whalen and Tuan-Hung Pham},
 year         = {2012},
 title        = {The {G}uardol Language and Verification System},
 booktitle    = {Proceedings of TACAS},
 series       = {LNCS},
 volume       = {7214},
 publisher    = {Springer},
 pages        = {18--32},
 doi          = {10.1007/978-3-642-28756-5_3},
)
@inproceedings(Harish2007,
 author       = {Parwan Harish and P.J. Narayanan},
 year         = {2007},
 title        = {Accelerating Large Graph Algorithms on the {GPU} using {CUDA}},
 booktitle    = {IEEE High Performance Computing -- HiPC 2007},
 series       = {LNCS},
 volume       = {4873},
 publisher    = {Springer},
 pages        = {197--208},
 doi          = {10.1007/978-3-540-77220-0\_21},
)
@book(acl2:book,
 author       = {Matt Kaufmann and Panagiotis Manolios and J Strother Moore},
 year         = {2000},
 title        = {Computer-Aided Reasoning: An Approach},
 series       = {Texts and Monographs in Computer Science},
 publisher    = {Kluwer Academic Publishers},
 doi          = {10.1007/978-1-4615-4449-4},
)
@inproceedings(cakeML:popl14,
 author       = {Ramana Kumar and Magnus O. Myreen and Michael Norrish and Scott Owens},
 year         = {2014},
 title        = {{CakeML}: A Verified Implementation of {ML}},
 booktitle    = {POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 publisher    = {ACM Press},
 pages        = {179--191},
 doi          = {10.1145/2535838.2535841},
)
@inproceedings(dafny:icse,
 author       = {K. Rustan M. Leino},
 year         = {2013},
 title        = {Developing Verified Programs with {D}afny},
 booktitle    = {Proceedings of the 2013 International Conference on Software Engineering},
 series       = {ICSE '13},
 publisher    = {IEEE Press},
 pages        = {1488--1490},
 doi          = {10.1109/icse.2013.6606754},
 url          = {http://dl.acm.org/citation.cfm?id=2486788.2487050},
)
@inproceedings(Boogie-IVL,
 author       = {K. Rustan M. Leino and P. Ruemmer},
 year         = {2010},
 title        = {A Polymorphic Intermediate Verification Language: Design and Logical Encoding},
 booktitle    = {Proceedings of TACAS},
 series       = {LNCS},
 volume       = {6015},
 pages        = {312--327},
 doi          = {10.1007/978-3-642-12002-2_26},
)
@article(leroy:cacm,
 author       = {Xavier Leroy},
 year         = {2009},
 title        = {Formal verification of a realistic compiler},
 journal      = {Communications of the {ACM}},
 volume       = {52},
 number       = {7},
 pages        = {107--115},
 doi          = {10.1145/1538788.1538814},
)
@book(sparkapps,
 author       = {John W McCormick and Peter C. Chapin},
 year         = {2015},
 title        = {Building High Integrity Applications with {SPARK}},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/cbo9781139629294},
)
@phdthesis(myreen:phd,
 author       = {Magnus Myreen},
 year         = {2009},
 title        = {Formal verification of machine-code programs},
 school       = {University of Cambridge},
)
@article(so-called-translator,
 author       = {Magnus O. Myreen and Scott Owens},
 year         = {2014},
 title        = {Proof-producing Translation of Higher-order logic into Pure and Stateful {ML}},
 journal      = {Journal of Functional Programming},
 volume       = {24},
 number       = {2-3},
 pages        = {284--315},
 doi          = {10.1017/S0956796813000282},
)
@inproceedings(MASC,
 author       = {John W. O'Leary and David M. Russinoff},
 year         = {2014},
 title        = {Modeling Algorithms in {SystemC} and {ACL2}},
 booktitle    = {Proceedings of the 12th International Workshop on the {ACL2} Theorem Prover and its Applications},
 volume       = {152},
 publisher    = {EPTCS},
 pages        = {145--162},
 doi          = {10.4204/EPTCS.152.12},
 url          = {https://arxiv.org/pdf/1406.1565.pdf},
)
@phdthesis(hung:phd,
 author       = {Tuan-Hung Pham},
 year         = {2014},
 title        = {Verification of Recursive Data Types using Abstractions},
 school       = {Department of Computer Science and Engineering, University of Minnesota},
)
@manual(DO-178C,
 organization = {{RTCA} {C}ommittee {SC}-205},
 year         = {2015},
 title        = {DO-178C Software Considerations in Airborne Systems and Equipment Certification},
 url          = {https://my.rtca.org/nc\_\_store?search=DO-178C},
)
@phdthesis(Schirmer-PhD,
 author       = {Norbert Schirmer},
 year         = {2006},
 title        = {Verification of sequential imperative programs in {I}sabelle/{HOL}},
 school       = {TU Munich},
)
@article(tolmach:ML,
 author       = {Andrew Tolmach and Dino P. Oliva},
 year         = {1998},
 title        = {From {ML} to {Ada}: Strongly-typed Language Interoperability via Source Translation},
 journal      = {Journal of Functional Programming},
 volume       = {8},
 number       = {4},
 pages        = {367 -- 412},
 doi          = {10.1017/s0956796898003086},
)
@inproceedings(typesbytes,
 author       = {Harvey Tuch and Gerwin Klein and Michael Norrish},
 year         = {2007},
 title        = {Types, Bytes, and Separation Logic},
 booktitle    = {Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 series       = {POPL '07},
 publisher    = {ACM Press},
 pages        = {97--108},
 doi          = {10.1145/1190216.1190234},
)