Trusted Certification Tools

逻辑是描述和推理数字系统的数学选择。将逻辑的机械化应用于具有实际重要性的人工制品仍处于起步阶段，最终将代表应用数学和计算机科学史上的重大发展。本研究旨在(a)提高特定机械定理证明系统（ACL2）的自动化和可扩展性，(b)演示这样的系统如何允许不受信任的承包商交付受信任的工件，以及(c)产生值得信赖的工业强度认证工具。这项工作将使不受信任的承包商能够交付相对孤立但仍然至关重要的软件包。随着越来越多的基础设施被编码，可以使用这种范式构建更大的分层可信系统。该工作进一步自动化了验证过程，并将降低获得交付系统满足指定需求的高保证所需的工作量。该技术的本科和研究生教学不断扩大正式方法的劳动力。ACL2在源代码级别免费分发，并提供大量文档，每年举办研讨会以分发社区获得的知识。

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.