Certifying Compositional Model Checking Algorithms in ACL2
Sandip Ray, John Matthews, and Mark Tuttle

---

We prove the soundness of a compositional model checking algorithm using ACL2. The algorithm uses conjunctive and cone of influence reductions to reduce a large model checking problem into a collection of smaller problems, and we prove the soundness of the composition of these reductions. The algorithm checks properties specified in Linear Temporal Logic (LTL), but the ACL2 logic does not allow us to express either the classical semantics of LTL or the classical soundness proofs for these reductions. We discuss an approach to circumvent such restrictions in ACL2. We also propose enhancements to ACL2 that would make similar proof attempts easier in the future. Finally, we argue in favor of providing better integration of ACL2 with external model checkers and other analysis tools.