Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehicle. - David S. Hardin; Matthew Wilding; David A. Greve (CAV, 1998)

Efficient Simulation of Formal Processor Models. - Matthew Wilding; David A. Greve; David S. Hardin (Formal Methods Syst. Des., 2001)

A robust machine code proof framework for highly secure applications. - David S. Hardin; Eric Whitman Smith; William D. Young (ACL2, 2006)

Invited Tutorial: Considerations in the Design and Verification of Microprocessors for Safety-Critical and Security-Critical Applications. - David S. Hardin (FMCAD, 2008)

Development of Security Software: A High Assurance Methodology. - David S. Hardin; T. Douglas Hiratzka; D. Randolph Johnson; Lucas G. Wagner; Michael W. Whalen (ICFEM, 2009)

Formal Verification of Partition Management for the AAMP7G Microprocessor. - Matthew Wilding; David A. Greve; Raymond J. Richards; David S. Hardin (Design and Verification of Microprocessor Systems for High-Assurance Applications, 2010)

Bakar Kiasan: Flexible Contract Checking for Critical Systems Using Symbolic Execution. - Jason Belt; John Hatcliff; Robby; Patrice Chalin; David S. Hardin; Xianghua Deng (NASA Formal Methods, 2011)

Enhancing spark's contract checking facilities using symbolic execution. - Jason Belt; John Hatcliff; Robby; Patrice Chalin; David S. Hardin; Xianghua Deng (SIGAda, 2011)

A DSL for cross-domain security. - David S. Hardin; Konrad Slind; Michael W. Whalen; Tuan-Hung Pham (HILT, 2012)

The Guardol Language and Verification System. - David S. Hardin; Konrad Slind; Michael W. Whalen; Tuan-Hung Pham (TACAS, 2012)

The Specification, Verification, and Implementation of a High-Assurance Data Structure: An ACL2 Approach. - David S. Hardin (HICSS, 2013)

ACL2 Meets the GPU: Formalizing a CUDA-based Parallelizable All-Pairs Shortest Path Algorithm in ACL2 - David S. Hardin; Samuel S. Hardin (ACL2, 2013)

Development of a Translator from LLVM to ACL2. - David S. Hardin; Jennifer A. Davis; David A. Greve; Jedidiah R. McClurg (ACL2, 2014)

Reasoning About LLVM Code Using Codewalker. - David S. Hardin (ACL2, 2015)

A High-Assurance, High-Performance Hardware-Based Cross-Domain System. - David S. Hardin; Konrad Slind; Mark Bortz; James Potts; Scott Owens (SAFECOMP, 2016)

Using ACL2 in the Design of Efficient, Verifiable Data Structures for High-Assurance Systems. - David S. Hardin; Konrad Slind (ACL2, 2018)

Synthesis of Verified Architectural Components for Critical Systems Hosted on a Verified Microkernel. - David S. Hardin (HICSS, 2020)

Formal Synthesis of Filter Components for Use in Security-Enhancing Architectural Transformations. - David S. Hardin; Konrad L. Slind (SP (Workshops), 2021)

Hardware/Software Co-Assurance using the Rust Programming Language and ACL2. - David S. Hardin (ACL2, 2022)

Cyberassured Systems Engineering at Scale. - Darren D. Cofer; Isaac Amundson; Junaid Babar; David S. Hardin; Konrad Slind; Perry Alexander; John Hatcliff; Robby; Gerwin Klein; Corey Lewis; Eric Mercer; John Shackleton (IEEE Secur. Priv., 2022)

Verification of a Rust Implementation of Knuth's Dancing Links using ACL2. - David S. Hardin (ACL2, 2023)

Model-driven development for the seL4 microkernel using the HAMR framework. - Jason Belt; John Hatcliff; Robby; John Shackleton; Jim Carciofini; Todd Carpenter; Eric Mercer; Isaac Amundson; Junaid Babar; Darren D. Cofer; David S. Hardin; Karl Hoech; et al. (J. Syst. Archit., 2023)

Synthesizing verified components for cyber assured systems engineering. - Eric Mercer; Konrad Slind; Isaac Amundson; Darren D. Cofer; Junaid Babar; David S. Hardin (Softw. Syst. Model., 2023)

Towards Explainable Compositional Reasoning. - Isaac Amundson; Amer Tahat; David S. Hardin; Darren D. Cofer (ERSA@RTSS, 2024)

Integrated Contract-Based Unit and System Testing for Component-Based Systems. - John Hatcliff; Jason Belt; Robby; David S. Hardin (NFM, 2024)

Proof Repair Utilizing Large Language Models: A Case Study on the Copland Remote Attestation Proofbase. - Amer Tahat; David S. Hardin; Adam Petz; Perry Alexander (AISoLA, 2024)

Zero-trust design and assurance patterns for cyber-physical systems. - Saqib Hasan; Isaac Amundson; David S. Hardin (J. Syst. Archit., 2024)