David S. Hardin

Publication Activity (10 Years)

Years Active: 1998-2024
Publications (10 Years): 10

Top Topics

Design Thinking

Computational Biology

Systems Engineering

Top Venues

Publications

John Hatcliff, Jason Belt, Robby, David S. Hardin
Integrated Contract-Based Unit and System Testing for Component-Based Systems. NFM (2024)
David S. Hardin
Verification of a Rust Implementation of Knuth's Dancing Links using ACL2. CoRR (2023)
Eric Mercer, Konrad Slind, Isaac Amundson, Darren D. Cofer, Junaid Babar, David S. Hardin
Synthesizing verified components for cyber assured systems engineering. Softw. Syst. Model. 22 (5) (2023)
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, Konrad Slind, Ihor Kuz, Kent McLeod
Model-driven development for the seL4 microkernel using the HAMR framework. J. Syst. Archit. 134 (2023)
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
Cyberassured Systems Engineering at Scale. IEEE Secur. Priv. 20 (3) (2022)
David S. Hardin, Konrad L. Slind
Formal Synthesis of Filter Components for Use in Security-Enhancing Architectural Transformations. SP Workshops (2021)
Eric Mercer, Konrad Slind, Isaac Amundson, Darren D. Cofer, Junaid Babar, David S. Hardin
Synthesizing Verified Components for Cyber Assured Systems Engineering. MoDELS (2021)
David S. Hardin
Synthesis of Verified Architectural Components for Critical Systems Hosted on a Verified Microkernel. HICSS (2020)
David S. Hardin, Konrad Slind
Using ACL2 in the Design of Efficient, Verifiable Data Structures for High-Assurance Systems. ACL2 (2018)
David S. Hardin, Konrad Slind, Mark Bortz, James Potts, Scott Owens
A High-Assurance, High-Performance Hardware-Based Cross-Domain System. SAFECOMP (2016)
David S. Hardin
Reasoning About LLVM Code Using Codewalker. ACL2 (2015)
David S. Hardin, Jennifer A. Davis, David A. Greve, Jedidiah R. McClurg
Development of a Translator from LLVM to ACL2. ACL2 (2014)
David S. Hardin, Samuel S. Hardin
ACL2 Meets the GPU: Formalizing a CUDA-based Parallelizable All-Pairs Shortest Path Algorithm in ACL2 ACL2 (2013)
David S. Hardin
The Specification, Verification, and Implementation of a High-Assurance Data Structure: An ACL2 Approach. HICSS (2013)
David S. Hardin, Konrad Slind, Michael W. Whalen, Tuan-Hung Pham
A DSL for cross-domain security. HILT (2012)
David S. Hardin, Konrad Slind, Michael W. Whalen, Tuan-Hung Pham
The Guardol Language and Verification System. TACAS (2012)
Jason Belt, John Hatcliff, Robby, Patrice Chalin, David S. Hardin, Xianghua Deng
Bakar Kiasan: Flexible Contract Checking for Critical Systems Using Symbolic Execution. NASA Formal Methods (2011)
Jason Belt, John Hatcliff, Robby, Patrice Chalin, David S. Hardin, Xianghua Deng
Enhancing spark's contract checking facilities using symbolic execution. SIGAda (2011)
David S. Hardin, T. Douglas Hiratzka, D. Randolph Johnson, Lucas G. Wagner, Michael W. Whalen
Development of Security Software: A High Assurance Methodology. ICFEM (2009)
David S. Hardin
Invited Tutorial: Considerations in the Design and Verification of Microprocessors for Safety-Critical and Security-Critical Applications. FMCAD (2008)
David S. Hardin, Eric W. Smith, William D. Young
A robust machine code proof framework for highly secure applications. ACL2 (2006)
Matthew Wilding, David A. Greve, David S. Hardin
Efficient Simulation of Formal Processor Models. Formal Methods Syst. Des. 18 (3) (2001)
David S. Hardin, Matthew Wilding, David A. Greve
Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehicle. CAV (1998)