Theorem Proving


Visible to the public Hardware/Software Coassurance using Algorithmic C and ACL2

Dr. David S. Hardin has made contributions in the areas of formal methods, computer architecture for High Assurance systems, as well as real-time and embedded Java. He is a Principal Research Engineer in the Advanced Technology Center at Rockwell Collins, and currently serves as a co-Principal Investigator for the DARPA CASE (Cyber Assured Systems Engineering) program.