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.
