Award Abstract #0429591
Trusted Certification Tools

NSF Org:	CNS Division of Computer and Network Systems
Initial Amendment Date:	May 6, 2005
Latest Amendment Date:	September 21, 2007
Award Number:	0429591
Award Instrument:	Standard Grant
Program Manager:	Karl N. Levitt CNS Division of Computer and Network Systems CSE Directorate for Computer & Information Science & Engineering
Start Date:	May 1, 2005
Expires:	April 30, 2009 (Estimated)
Awarded Amount to Date:	$2097966
Investigator(s):	Warren Hunt, Jr. hunt@cs.utexas.edu (Principal Investigator) J Strother Moore (Co-Principal Investigator)
Sponsor:	University of Texas at Austin P.O Box 7726 Austin, TX 78713 512/471-6424
NSF Program(s):	,
Field Application(s):	0000912 Computer Science
Program Reference Code(s):	HPCC,9218,7456,7254
Program Element Code(s):	V933,V901,T951,T508

ABSTRACT

Logic is the mathematics of choice for describing and reasoning about digital systems. The mechanized application of logic to artifacts of practical importance is still in its infancy and will ultimately represent a major development in the history of applied mathematics and computer science. This research aims to (a) increase the automation and scalability of a particular mechanical theorem-proving system (ACL2), (b) demonstrate how such a system allows an untrusted contractor to deliver a trusted artifact, and (c) produce a trustworthy, industrial-strength certification tool.

The work will enable untrusted contractors to deliver relatively isolated but still-critical software packages. As more infrastructure is codified, larger hierarchical trusted systems can be built with this paradigm. The work further automates the validation process and will lower the effort required to attain high assurance that a delivered system meets specified requirements. Undergraduate and graduate teaching of this technology continues to enlarge the formal methods workforce. ACL2 is freely distributed at the source-code level, with extensive documentation, and annual workshops are held to distribute the community's acquired knowledge.

PUBLICATIONS PRODUCED AS A RESULT OF THIS RESEARCH

Next (Showing: 1 - 20 of 27).

David A. Greve, Matt Kaufmann, Panagiotis Manolios, J Strother Moore, Sandip Ray, Jose Luis Ruiz-Reina, Robert Sumners, Daron.  "Efficient Execution in an Automated Reasoning Environment,"  Journal of Functional Programming,  v.18,  2008,  p. 1.

David Rager.  "Adding Parallelism Capabilities to ACL2,"  6th International Workshop on the ACL2 Theorem Prover and Its Applications,  v.205/ACM,  2006,  p. 90-94.

David S. Hardin, Eric W. Smith, William D. Young.  "A Robust Machine Code Proof Framework for Highly Secure Applications,"  6th International Workshop on the ACL2 Theorem Prover and Its Applications,  v.205/ACM,  2006,  p. 11-20.

Erik Reeber and Jun Sawada.  "Combining ACL2 and an automated verification tool to verify a multiplier,"  6th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2006),  v.205/ACM,  2006,  p. 63-70.

Erik Reeber and Warren A. Hunt, Jr..  "A SAT-Based Procedure for Verifying Finite State Machines in ACL2,"  6th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2006),  v.205/ACM,  2006,  p. 127-135.

Erik Reeber and Warren A. Hunt, Jr..  "A SAT-Based Decision Procedure for the Subclass of Unrollable List Functions in ACL2 (SULFA),"  LNCS [3rd International Joint Conference on Automated Reasoning (IJCAR 2006)],  v.4130,  2007,  p. 453-467.

Jared Davis.  "Reasoning about ACL2 file input,"  6th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2006),  v.205/ACM,  2006,  p. 117-126.

Jared Davis.  "Memories: array-like records for ACL2,"  6th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2006),  v.205/ACM,  2006,  p. 57-60.

Jayanta Bhadra, Magdy Abadir, Li-C Wang, and Sandip Ray.  "A Survey of Hybrid Techniques for Functional Verification,"  IEEE Design and Test of Computers,  v.24(2),  2007,  p. 112-122.

John Erickson.  "Backtracking in ACL2,"  Proceedings of the 7th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2007),  2007, 

John Matthews, J Strother Moore, Sandip Ray, Daron Vroon.  "Verification Condition Generation via Theorem Proving,"  13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2006),  v.4246 of,  2006,  p. 362-376.

Jun Sawada and Erik Reeber.  "ACL2SIX: A Hint used to Integrate a Theorem Prover and an Automated Verification Tool,"  Sixth Conference on Formal Methods in Computer-Aided Design (FMCAD 2006),  2007,  p. 453-467.

Matt Kaufmann and J Strother Moore.  "Double Rewriting for Equivalential Reasoning in ACL2,"  6th International Workshop on the ACL2 Theorem Prover and Its Applications,  v.205/ACM,  2006,  p. 103-106.

Matt Kaufmann and Konrad Slind.  "Proof Pearl: Wellfounded Induction on the Ordinals up to Epsilon-0,"  TPHOLS 2007,  v.LNCS 47,  2007,  p. 494.

Matt Kaufmann, J Strother Moore, Sandip Ray and Erik Reeber.  "Integrating External Deduction Tools with ACL2,"  6th International Workshop on Implementation of Logics (IWIL 2006), CEUR Workshop Proceedings,  v.212,  2006,  p. 7-26.

Matt Kaufmann, Panagiotis Manolios, J Strother Moore, and Daron Vroon.  "Integrating CCG analysis into ACL2,"  Proceedings of The Eighth International Workshop on Termination,  v.8,  2006,  p. 64-68.

Michael J.C. Gordon, Warren A. Hunt, Jr., Matt Kaufmann, and James Reynolds.  "An Integration of HOL and ACL2,"  Proceedings of the 6th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2006),  2006,  p. 153-160.

Michael J.C. Gordon, Warren A. Hunt, Jr., Matt Kaufmann, and James Reynolds.  "An Embedding of the ACL2 Logic in HOL,"  6th International Workshop on the ACL2 Theorem Prover and Its Applications,  v.205/ACM,  2006,  p. 40-46.

Peter Dillinger, Matt Kaufmann, and Panagiotis Manolios.  "Hacking and Extending ACL2,"  Proceedings of the 7th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2007),  2007,  p. 1.

Sandip Ray.  "Quantification in Tail-recursive Function Definitions,"  6th International Workshop on the ACL2 Theorem Prover and Its Applications,  v.205/ACM,  2006,  p. 95-98.


Next (Showing: 1 - 20 of 27).

Please report errors in award information by writing to: awardsearch@nsf.gov.