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.