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.
