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

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

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.