Computational ""proof assistants,"" which allow users to construct axiomatic proofs of formally specified assertions, are currently used for two purposes: first, to verify ordinary mathematical proofs, and second, to verify that (descriptions of) hardware and software meet design specifications. This project will develop logical and computational methods to support both types of activities. Specific components of the project include: the development of formal libraries to support proofs in number theory and discrete geometry; the extraction of verification conditions from software component specifications and implementations in an assertive programming language known as Resolve; a classification of the types of inferences that arise in both domains; the development of logical methods for verifying these inferences automatically; and the development of educational materials and software that will make it possible to integrate these methods into undergraduate and graduate curricula in computer science and mathematics.

As mathematical proofs become more and more intricate, and now often rely on extensive computation, it is becoming increasingly difficult to verify that they are correct. Similarly, as hardware and software systems become more and more complex, it is becoming increasingly difficult to verify that they meet their design specifications. Doing so is especially important when resources, lives, and security depend on their correct behavior. This collaboration between mathematical logicians and computer scientists will develop methods to make it possible to verify that such mathematical and computational claims are valid, and that the arguments supporting them are free of errors. The project will also develop means of training the next generation of computer scientists and mathematicians to use these methods.

Agency
National Science Foundation (NSF)
Institute
Division of Mathematical Sciences (DMS)
Type
Standard Grant (Standard)
Application #
0701187
Program Officer
Tomek Bartoszynski
Project Start
Project End
Budget Start
2007-09-01
Budget End
2010-08-31
Support Year
Fiscal Year
2007
Total Cost
$54,999
Indirect Cost
Name
Clemson University
Department
Type
DUNS #
City
Clemson
State
SC
Country
United States
Zip Code
29634