SHF: Medium: Generating Correctness Proofs with Neural Networks

University Of California-San Diego, La Jolla CA

Investigators

Abstract

Errors in software can lead to disastrous consequences, from power outages to stock market crashes, and from massive leaks of private consumer data to wide-scale software vulnerabilities. A promising approach to making software more reliable is foundational verification. In this approach programmers use a theorem prover to state and prove properties about their programs. Because the proofs are done with the assistance of a theorem prover, in full complete detail, foundational verification provides the strongest possible levels of assurance, virtually guaranteeing that the software works correctly. However, while foundational verification shows great promise, the cost of producing foundationally verified software remains prohibitively high for most programs, as it requires enormous manual effort by highly trained experts. The manual effort required in foundational verification is one of the main impediments to the broader adoption of this promising technique. The goal of this project is to use machine learning to significantly alleviate the manual effort required to complete proofs in foundational verification, thereby fundamentally reshaping the cost/benefit analysis of using the methodology. The intellectual merit involves training machine-learning algorithms on current proofs to automatically predict the steps that need to be taken in future proofs. By laying the foundation for a significant shift in the cost/benefit analysis of using foundational verification, this project has the potential of ushering in an new era of increased adoption of the technique, and of safer and more secure software as a result. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.