David S. Hardin

32 papers A* 1A 2B 2C 2Journal 5Unranked 17

Year	Rank	Type	Title / Venue / Authors
2025	—	`conf`	AGREE-Dog Copilot: A Neuro-Symbolic Approach to Enhanced Model-Based Systems Engineering. AISoLA Amer Tahat, Isaac Amundson, David S. Hardin, Darren D. Cofer
2025	C	`conf`	Proof Engineering in Logika: Synergistically Integrating Automated and Semi-automated Program Verification. FMICS Stefan Hallerstede, Robby, John Hatcliff, Jason Belt, David S. Hardin
2024	—	`conf`	Integrated Contract-Based Unit and System Testing for Component-Based Systems. NFM John Hatcliff, Jason Belt, Robby, David S. Hardin
2024	—	`conf`	Proof Repair Utilizing Large Language Models: A Case Study on the Copland Remote Attestation Proofbase. AISoLA Amer Tahat, David S. Hardin, Adam Petz, Perry Alexander
2024	—	`conf`	Towards Explainable Compositional Reasoning. ERSA@RTSS Isaac Amundson, Amer Tahat, David S. Hardin, Darren D. Cofer
2024	J	`jnl`	Zero-trust design and assurance patterns for cyber-physical systems. J. Syst. Archit. Saqib Hasan, Isaac Amundson, David S. Hardin
2023	J	`jnl`	Model-driven development for the seL4 microkernel using the HAMR framework. J. Syst. Archit. 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
2023	J	`jnl`	Synthesizing verified components for cyber assured systems engineering. Softw. Syst. Model. Eric Mercer, Konrad Slind, Isaac Amundson, Darren D. Cofer, Junaid Babar, David S. Hardin
2023	—	`conf`	Verification of a Rust Implementation of Knuth's Dancing Links using ACL2. ACL2 David S. Hardin
2022	J	`jnl`	Cyberassured Systems Engineering at Scale. IEEE Secur. Priv. 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
2022	—	`conf`	Hardware/Software Co-Assurance using the Rust Programming Language and ACL2. ACL2 David S. Hardin
2021	—	`conf`	Formal Synthesis of Filter Components for Use in Security-Enhancing Architectural Transformations. SP (Workshops) David S. Hardin, Konrad L. Slind
2021	A	`conf`	Synthesizing Verified Components for Cyber Assured Systems Engineering. MoDELS Eric Mercer, Konrad Slind, Isaac Amundson, Darren D. Cofer, Junaid Babar, David S. Hardin
2020	—	`conf`	Synthesis of Verified Architectural Components for Critical Systems Hosted on a Verified Microkernel. HICSS David S. Hardin
2018	—	`conf`	Using ACL2 in the Design of Efficient, Verifiable Data Structures for High-Assurance Systems. ACL2 David S. Hardin, Konrad Slind
2016	B	`conf`	A High-Assurance, High-Performance Hardware-Based Cross-Domain System. SAFECOMP David S. Hardin, Konrad Slind, Mark Bortz, James Potts, Scott Owens
2015	—	`conf`	Reasoning About LLVM Code Using Codewalker. ACL2 David S. Hardin
2014	—	`conf`	Development of a Translator from LLVM to ACL2. ACL2 David S. Hardin, Jennifer A. Davis, David A. Greve, Jedidiah R. McClurg
2013	—	`conf`	ACL2 Meets the GPU: Formalizing a CUDA-based Parallelizable All-Pairs Shortest Path Algorithm in ACL2 ACL2 David S. Hardin, Samuel S. Hardin
2013	—	`conf`	The Specification, Verification, and Implementation of a High-Assurance Data Structure: An ACL2 Approach. HICSS David S. Hardin
2012	—	`conf`	A DSL for cross-domain security. HILT David S. Hardin, Konrad Slind, Michael W. Whalen, Tuan-Hung Pham
2012	A	`conf`	The Guardol Language and Verification System. TACAS David S. Hardin, Konrad Slind, Michael W. Whalen, Tuan-Hung Pham
2011	—	`conf`	Bakar Kiasan: Flexible Contract Checking for Critical Systems Using Symbolic Execution. NASA Formal Methods Jason Belt, John Hatcliff, Robby, Patrice Chalin, David S. Hardin, Xianghua Deng
2011	—	`conf`	Enhancing spark's contract checking facilities using symbolic execution. SIGAda Jason Belt, John Hatcliff, Robby, Patrice Chalin, David S. Hardin, Xianghua Deng
2011	—	`ed.`	Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2011, Austin, Texas, USA, November 3-4, 2011. ACL2 David S. Hardin, Julien Schmaltz
2010	—	`book`	Design and Verification of Microprocessor Systems for High-Assurance Applications. David S. Hardin
2010	—	`ch.`	Formal Verification of Partition Management for the AAMP7G Microprocessor. Design and Verification of Microprocessor Systems for High-Assurance Applications Matthew Wilding, David A. Greve, Raymond J. Richards, David S. Hardin
2009	C	`conf`	Development of Security Software: A High Assurance Methodology. ICFEM David S. Hardin, T. Douglas Hiratzka, D. Randolph Johnson, Lucas G. Wagner, Michael W. Whalen
2008	B	`conf`	Invited Tutorial: Considerations in the Design and Verification of Microprocessors for Safety-Critical and Security-Critical Applications. FMCAD David S. Hardin
2006	—	`conf`	A robust machine code proof framework for highly secure applications. ACL2 David S. Hardin, Eric Whitman Smith, William D. Young
2001	J	`jnl`	Efficient Simulation of Formal Processor Models. Formal Methods Syst. Des. Matthew Wilding, David A. Greve, David S. Hardin
1998	A*	`conf`	Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehicle. CAV David S. Hardin, Matthew Wilding, David A. Greve