Certifying Compositional Model Checking Algorithms in ACL2

S. Ray, J. Matthews , and M. Tuttle

In W. A. Hunt, Jr., M. Kaufmann, and J S. Moore, editors, 4th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2003), Boulder, CO, July 2003

Abstract

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 future. Finally, we argue in favor of providing better integration of ACL2 with external model checkers and other analysis tools.

Relevant files

Paper (ps, pdf)
Slides for ACL2 2003 (ps, pdf, ppt)
Supporting materials: See the directory books/workshops/2003/ray-matthews-tuttle/support/ in the current ACL2 distribution. (Note: You need the workshops tarball. See the instructions for installing ACL2 in the ACL2 homepage.)

BibTex

@Inproceedings{ray-certifying,
  title     = "{Certifying Compositional Model Checking Algorithms in ACL2}",
  author    = "S. Ray and J. Matthews and M. Tuttle",
  editor    = "Hunt, Jr., W. A. and M. Kaufmann and J S. Moore",
  booktitle = "{$4$th International Workshop on the ACL2 Theorem Prover and Its Applications
                (ACL2 2003)}",
  address   = "{Boulder, CO}",
  month     = jul,
  year      = "2003"
}