TC: EAGER: Modularization Supporting Extensibility for an Industrial-strength Theorem Prover

ACL 2定理证明器在工业、政府和学术界都有一个成熟的用户社区。 ACL 2通过结合自动化和可控性来支持工业规模的验证项目，但其可扩展性有限：其庞大（10 MB），复杂的代码库要求，为了可靠性，它只能委托给它的两个作者。 PI建议从根本上修改ACL 2，通过使其更加模块化来开放ACL，从而使不受信任的用户能够进行可信开发，同时保持证明安全性。 关键的挑战是公开系统组件的功能，并将受信任的核心与不需要被信任以实现正确功能的代码分离，例如实现逻辑、I/O、理论管理和交互式证明开发和调试的代码。 代码重构已经是一个很难的问题，特别是对于一个具有ACL 2复杂性的系统，但是在这个项目中，还有一个挑战，就是使最终的系统在不损害逻辑合理性的情况下是可修改的。预期的结果包括一个ACL 2系统，它可以由用户根据特定的需求进行合理的修改。 特别是，研究梳理除了固有的顺序输出推理代码应该支持并行推理算法的研究，利用现代多核机器，导致正式验证并行实现。 更一般地说，该系统将提供一个平台，促进自动推理的数学研究。 它还便于定制ACL 2，以便在本科生课堂上使用。 由此产生的系统将在互联网上免费分发。

The ACL2 theorem prover has an established user community in industry,government, and academia. ACL2 supports industrial-scale verificationprojects by combining automation and controllability, but itsextensibility is limited: its large (10 MB), complex code baserequires, for soundness, that it be entrusted solely to its twoauthors. The PIs propose to modify ACL2 radically, opening up thesystem by making it more modular, thus enabling trusted development byuntrusted users while maintaining proof security. Key challenges areto expose the functionality of system components, and to separate outa trusted core from code that need not be trusted for correctfunctionality, such as code implementing heuristics, I/O, theorymanagement, and interactive proof development and debugging. Coderefactoring is already a hard problem, especially for a system withthe complexity of ACL2, but in this project there is also thechallenge of making the resulting system modifiable in a way that doesnot compromise logical soundness.Expected results include an ACL2 system that can be modified soundlyby users according to specific needs. In particular, research onteasing apart inherently sequential output from reasoning code shouldsupport research on parallel reasoning algorithms taking advantage ofmodern multi-core machines, leading to formally verified parallelimplementations. More generally, the system will provide a platformthat promotes research in heuristics for automating reasoning. Itwill also facilitate the customization of ACL2 for use in theundergraduate classroom. The resulting system will be freelydistributed on the Internet.