##
**Combining symmetry reduction and under-approximation for symbolic model checking.**
*(English)*
Zbl 1010.68510

Brinksma, Ed (ed.) et al., Computer aided verification. 14th international conference, CAV 2002, Copenhagen, Denmark, July 27-31, 2002. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2404, 93-106 (2002).

Summary: This work presents a collection of methods, integrating symmetry reduction, under-approximation, and symbolic model checking in order to reduce space and time for model checking. The main goal of this work is falsification. However, under certain conditions our methods provide verification as well.

We first present algorithms that perform on-the-fly model checking for temporal safety properties, using symmetry reduction. We then extend these algorithms for checking liveness properties as well.

Our methods are fully automatic. The user should supply some basic information about the symmetry in the verified system. However, the methods are robust and work correctly even if the information supplied by the user is incorrect. Moreover, the methods return correct results even in case the computation of the symmetry reduction has not been completed due to memory or time explosion.

We implemented our methods within IBM’s model checker RuleBase, and compared the performance of our methods with that of RuleBase. In most cases, our algorithms outperformed RuleBase with respect to both time and space.

For the entire collection see [Zbl 0993.00049].

We first present algorithms that perform on-the-fly model checking for temporal safety properties, using symmetry reduction. We then extend these algorithms for checking liveness properties as well.

Our methods are fully automatic. The user should supply some basic information about the symmetry in the verified system. However, the methods are robust and work correctly even if the information supplied by the user is incorrect. Moreover, the methods return correct results even in case the computation of the symmetry reduction has not been completed due to memory or time explosion.

We implemented our methods within IBM’s model checker RuleBase, and compared the performance of our methods with that of RuleBase. In most cases, our algorithms outperformed RuleBase with respect to both time and space.

For the entire collection see [Zbl 0993.00049].

### MSC:

68Q60 | Specification and verification (program logics, model checking, etc.) |