|M.Sc Student||Keidar Sharon|
|Subject||Combining Symmetry Reduction and Under-Approximation for|
Symbolic Model Checking
|Department||Department of Computer Science||Supervisor||Professor 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.