Andrew W. Appel (2014):
Program Logics for Certified Compilers.
Cambridge University Press,
doi:10.1017/CBO9781107256552.
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.
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.
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.
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.
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.
David S. Hardin (2010):
Design and Verification of Microprocessor Systems for High-Assurance Applications.
Springer,
doi:10.1007/978-1-4419-1539-9.
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.
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.
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.
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.
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.
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.
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.
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.
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.
Xavier Leroy (2009):
Formal verification of a realistic compiler.
Communications of the ACM 52(7),
pp. 107–115,
doi:10.1145/1538788.1538814.
John W McCormick & Peter C. Chapin (2015):
Building High Integrity Applications with SPARK.
Cambridge University Press,
doi:10.1017/cbo9781139629294.
Magnus Myreen (2009):
Formal verification of machine-code programs.
University of Cambridge.
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.
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 https://arxiv.org/pdf/1406.1565.pdf.
Tuan-Hung Pham (2014):
Verification of Recursive Data Types using Abstractions.
Department of Computer Science and Engineering, University of Minnesota.
Norbert Schirmer (2006):
Verification of sequential imperative programs in Isabelle/HOL.
TU Munich.
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.
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.
eptcs@eptcs.org