Different directions in parallel and distributed model checking Orna Grumberg
Model checking procedures have already proved
useful for system verification. They are successfully applied
to find subtle bugs in complex system. However, they are limited
to medium size systems because of their high space requirements.
Many approaches to overcome this problem have been suggested.
In recent years there has been a growing interest in parallelizing
the model checking problem, thus obtaining greater space capacity
and computation power.
In this talk we will survey some of the approaches to parallelizing
different aspects of model checking. We will consider algorithms
that handle reachability, as well as LTL, CTL and Mucalculus
model checking. We will mention symbolic as well as explicit
algorithms. We will also refer to parallelizing operations
on BDDs, which is the data structure used in symbolic model checking.
