David S. Hardin

According to our database, David S. Hardin authored at least 23 papers between 1998 and 2023.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

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., October, 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, Konrad Slind, Ihor Kuz, Kent McLeod

J. Syst. Archit., 2023

Verification of a Rust Implementation of Knuth's Dancing Links using ACL2.

David S. Hardin

Proceedings of the 18th International Workshop on the ACL2 Theorem Prover and Its Applications, 2023

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

Hardware/Software Co-Assurance using the Rust Programming Language and ACL2.

David S. Hardin

Proceedings of the Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications, 2022

2021

Formal Synthesis of Filter Components for Use in Security-Enhancing Architectural Transformations.

David S. Hardin, Konrad L. Slind

Proceedings of the IEEE Security and Privacy Workshops, 2021

2020

Synthesis of Verified Architectural Components for Critical Systems Hosted on a Verified Microkernel.

David S. Hardin

Proceedings of the 53rd Hawaii International Conference on System Sciences, 2020

2018

Using ACL2 in the Design of Efficient, Verifiable Data Structures for High-Assurance Systems.

David S. Hardin, Konrad Slind

Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, 2018

2016

A High-Assurance, High-Performance Hardware-Based Cross-Domain System.

David S. Hardin, Konrad Slind, Mark Bortz, James Potts, Scott Owens

Proceedings of the Computer Safety, Reliability, and Security, 2016

2015

Reasoning About LLVM Code Using Codewalker.

David S. Hardin

Proceedings of the Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, 2015

2014

Development of a Translator from LLVM to ACL2.

David S. Hardin, Jennifer A. Davis, David A. Greve, Jedidiah R. McClurg

Proceedings of the Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, 2014

2013

ACL2 Meets the GPU: Formalizing a CUDA-based Parallelizable All-Pairs Shortest Path Algorithm in ACL2

David S. Hardin, Samuel S. Hardin

Proceedings of the Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, 2013

The Specification, Verification, and Implementation of a High-Assurance Data Structure: An ACL2 Approach.

David S. Hardin

Proceedings of the 46th Hawaii International Conference on System Sciences, 2013

2012

The Guardol Language and Verification System.

David S. Hardin, Konrad Slind, Michael W. Whalen, Tuan-Hung Pham

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2012

A DSL for cross-domain security.

David S. Hardin, Konrad Slind, Michael W. Whalen, Tuan-Hung Pham

Proceedings of the 2012 ACM Conference on High Integrity Language Technology, 2012

2011

Enhancing spark's contract checking facilities using symbolic execution.

Jason Belt, John Hatcliff, Robby, Patrice Chalin, David S. Hardin, Xianghua Deng

Proceedings of the 2011 Annual ACM SIGAda International Conference on Ada, 2011

Bakar Kiasan: Flexible Contract Checking for Critical Systems Using Symbolic Execution.

Jason Belt, John Hatcliff, Robby, Patrice Chalin, David S. Hardin, Xianghua Deng

Proceedings of the NASA Formal Methods, 2011

2010

Formal Verification of Partition Management for the AAMP7G Microprocessor.

Matthew Wilding, David A. Greve, Raymond J. Richards, David S. Hardin

Proceedings of the Design and Verification of Microprocessor Systems for High-Assurance Applications., 2010

2009

Development of Security Software: A High Assurance Methodology.

David S. Hardin, T. Douglas Hiratzka, D. Randolph Johnson, Lucas G. Wagner, Michael W. Whalen

Proceedings of the Formal Methods and Software Engineering, 2009

2008

Invited Tutorial: Considerations in the Design and Verification of Microprocessors for Safety-Critical and Security-Critical Applications.

David S. Hardin

Proceedings of the Formal Methods in Computer-Aided Design, 2008

2006

A robust machine code proof framework for highly secure applications.

David S. Hardin, Eric W. Smith, William D. Young

Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, 2006

2001

Efficient Simulation of Formal Processor Models.

Matthew Wilding, David A. Greve, David S. Hardin

Formal Methods Syst. Des., 2001

1998

Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehicle.

David S. Hardin, Matthew Wilding, David A. Greve

Proceedings of the Computer Aided Verification, 10th International Conference, 1998