| ACL2 is a theorem prover for a Common LISP-based programming language. It is widely used in industry for verifying computer systems such as virtual machines. Modular ACL2, which extends ACL2 with interfaces and modules, is designed for verification of large programs by allowing programmers to reason separately about individual components. This thesis presents an in-depth case study of Modular ACL2 and provides new conclusions about it. |
