The ACL2 theorem prover has an established user community in industry, government, and academia. ACL2 supports industrial-scale verification projects by combining automation and controllability, but its extensibility is limited: its large (10 MB), complex code base requires, for soundness, that it be entrusted solely to its two authors. The PIs propose to modify ACL2 radically, opening up the system by making it more modular, thus enabling trusted development by untrusted users while maintaining proof security. Key challenges are to expose the functionality of system components, and to separate out a trusted core from code that need not be trusted for correct functionality, such as code implementing heuristics, I/O, theory management, and interactive proof development and debugging. Code refactoring is already a hard problem, especially for a system with the complexity of ACL2, but in this project there is also the challenge of making the resulting system modifiable in a way that does not compromise logical soundness.
Expected results include an ACL2 system that can be modified soundly by users according to specific needs. In particular, research on teasing apart inherently sequential output from reasoning code should support research on parallel reasoning algorithms taking advantage of modern multi-core machines, leading to formally verified parallel implementations. More generally, the system will provide a platform that promotes research in heuristics for automating reasoning. It will also facilitate the customization of ACL2 for use in the undergraduate classroom. The resulting system will be freely distributed on the Internet.
