Trusted Certification Tools

逻辑是一种数学，用于描述和推理数字系统。 将逻辑机械化应用于具有实际重要性的人工制品仍处于起步阶段，最终将代表应用数学和计算机科学历史上的一个重大发展。 本研究的目的是（a）提高一个特定的机械定理证明系统（ACL 2）的自动化和可扩展性，（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.