1. Andrew W. Appel (2014): Program Logics for Certified Compilers. Cambridge University Press, doi:10.1017/CBO9781107256552.
  2. Jason Belt, John Hatcliff, Robby, Patrice Chalin, David S. Hardin & Xianghua Deng (2011): Bakar Kiasan: Flexible Contract Checking for Critical Systems using Symbolic Execution. In: Proceedings of the Third NASA Formal Methods Symposium (NFM 2011), pp. 58 – 72, doi:10.1007/978-3-642-20398-5_6.
  3. Robert S. Boyer & J Strother Moore (2002): Single-Threaded Objects in ACL2. In: Practical Aspects of Declarative Languages, 4th International Symposium, PADL 2002, LNCS 2257. Springer, pp. 9–27, doi:10.1007/3-540-45587-6_3.
  4. Adam Chlipala (2013): The Bedrock Structured Programming System: Combining Generative Metaprogramming and Hoare Logic in an Extensible Program Verifier. In: Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, ICFP '13. ACM Press, pp. 391–402, doi:10.1145/2500365.2500592.
  5. Jean-Christophe Filliâtre & Andrei Paskevich (2013): Why3 — Where Programs Meet Provers. In: Matthias Felleisen & Philippa Gardner: Proceedings of the 22nd European Symposium on Programming, LNCS 7792. Springer, pp. 125–128, doi:10.1007/978-3-642-37036-6_8.
  6. David Greenaway, Japheth Lim, June Andronick & Gerwin Klein (2014): Don't Sweat the Small Stuff: Formal Verification of C Code Without the Pain. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '14. ACM Press, pp. 429–439, doi:10.1145/2594291.2594296.
  7. David S. Hardin (2010): Design and Verification of Microprocessor Systems for High-Assurance Applications. Springer, doi:10.1007/978-1-4419-1539-9.
  8. David S. Hardin & Samuel S. Hardin (2009): Efficient, Formally Verifiable Data Structures using ACL2 Single-Threaded Objects for High-Assurance Systems. In: S. Ray & D. Russinoff: Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications. ACM Press, pp. 100 – 105, doi:10.1145/1637837.1637853.
  9. David S. Hardin & Samuel S. Hardin (2013): ACL2 Meets the GPU: Formalizing a CUDA-based Parallelizable All-Pairs Shortest Path Algorithm in ACL2. In: R. Gamboa & J. Davis: Proceedings of the 11th International Workshop on the ACL2 Theorem Prover and its Applications 114. EPTCS, pp. 127 – 142, doi:10.4204/EPTCS.114.10.
  10. David S. Hardin, T. Douglas Hiratzka, D. Randolph Johnson, Lucas G. Wagner & Michael W. Whalen (2009): Development of Security Software: A High Assurance Methodology. In: K. Breitman & A. Cavalcanti: Proceedings of the 11th International Conference on Formal Engineering Methods: Formal Methods and Software Engineering (ICFEM'09). Springer, pp. 266 – 285, doi:10.1007/978-3-642-10373-5_14.
  11. David S. Hardin, Konrad L. Slind, Mark A. Bortz, James Potts & Scott Owens (2016): A High-Assurance, High-Performance Hardware-Based Cross-Domain System. In: Computer Safety, Reliability, and Security - 35th International Conference, SAFECOMP 2016, LNCS 9922. Springer, pp. 102–113, doi:10.1007/978-3-319-45477-1_9.
  12. David S. Hardin, Konrad L. Slind, Michael W. Whalen & Tuan-Hung Pham (2012): The Guardol Language and Verification System. In: Proceedings of TACAS, LNCS 7214. Springer, pp. 18–32, doi:10.1007/978-3-642-28756-5_3.
  13. Parwan Harish & P.J. Narayanan (2007): Accelerating Large Graph Algorithms on the GPU using CUDA. In: IEEE High Performance Computing – HiPC 2007, LNCS 4873. Springer, pp. 197–208, doi:10.1007/978-3-540-77220-0_21.
  14. Matt Kaufmann, Panagiotis Manolios & J Strother Moore (2000): Computer-Aided Reasoning: An Approach. Texts and Monographs in Computer Science. Kluwer Academic Publishers, doi:10.1007/978-1-4615-4449-4.
  15. Ramana Kumar, Magnus O. Myreen, Michael Norrish & Scott Owens (2014): CakeML: A Verified Implementation of ML. In: POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, pp. 179–191, doi:10.1145/2535838.2535841.
  16. K. Rustan M. Leino (2013): Developing Verified Programs with Dafny. In: Proceedings of the 2013 International Conference on Software Engineering, ICSE '13. IEEE Press, pp. 1488–1490, doi:10.1109/icse.2013.6606754. Available at
  17. K. Rustan M. Leino & P. Ruemmer (2010): A Polymorphic Intermediate Verification Language: Design and Logical Encoding. In: Proceedings of TACAS, LNCS 6015, pp. 312–327, doi:10.1007/978-3-642-12002-2_26.
  18. Xavier Leroy (2009): Formal verification of a realistic compiler. Communications of the ACM 52(7), pp. 107–115, doi:10.1145/1538788.1538814.
  19. John W McCormick & Peter C. Chapin (2015): Building High Integrity Applications with SPARK. Cambridge University Press, doi:10.1017/cbo9781139629294.
  20. Magnus Myreen (2009): Formal verification of machine-code programs. University of Cambridge.
  21. Magnus O. Myreen & Scott Owens (2014): Proof-producing Translation of Higher-order logic into Pure and Stateful ML. Journal of Functional Programming 24(2-3), pp. 284–315, doi:10.1017/S0956796813000282.
  22. John W. O'Leary & David M. Russinoff (2014): Modeling Algorithms in SystemC and ACL2. In: Proceedings of the 12th International Workshop on the ACL2 Theorem Prover and its Applications 152. EPTCS, pp. 145–162, doi:10.4204/EPTCS.152.12. Available at
  23. Tuan-Hung Pham (2014): Verification of Recursive Data Types using Abstractions. Department of Computer Science and Engineering, University of Minnesota.
  24. RTCA Committee SC-205 (2015): DO-178C Software Considerations in Airborne Systems and Equipment Certification. Available at
  25. Norbert Schirmer (2006): Verification of sequential imperative programs in Isabelle/HOL. TU Munich.
  26. Andrew Tolmach & Dino P. Oliva (1998): From ML to Ada: Strongly-typed Language Interoperability via Source Translation. Journal of Functional Programming 8(4), pp. 367 – 412, doi:10.1017/s0956796898003086.
  27. Harvey Tuch, Gerwin Klein & Michael Norrish (2007): Types, Bytes, and Separation Logic. In: Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '07. ACM Press, pp. 97–108, doi:10.1145/1190216.1190234.

Comments and questions to:
For website issues: