M.Sc Thesis

M.Sc StudentKeidar Sharon
SubjectCombining Symmetry Reduction and Under-Approximation for
Symbolic Model Checking
DepartmentDepartment of Computer Science
Supervisor PROFESSOR EMERITUS Orna Grumberg


This work presents a collection of methods that integrate 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.

These algorithms avoid building the orbit relation and choose representatives on-the-fly while computing the reachable states.

We then extend these algorithms to check liveness properties as well.

In addition, we introduce another iterative on-the-fly algorithm  that builds subsets of the orbit relation rather than the full relation.

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 when 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.