# 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"
}