Efficient model-checking using partial order reductions
- DIMACS Center - Room 431
- Busch Campus
- Piscataway, New Jersey
- October 11, 1995 at 4:30 PM
Abstract:
Checking the correctness of concurrent programs is in
particular important due to the intricacy of the total effect of
parallel activities. This is unfortunately reflected also in the
complexity of performing the automatic verification of such programs,
resulting in a severe state explosion problem. In pursuit of being
able to verify bigger and more complicated concurrent programs,
the commutativity aspect of concurrency is exploited: a family of
verification techniques, called `partial order reductions' alleviates
the state explosion problem, achieving more efficient verification of
concurrent programs.
In this talk, several recent new results of partial order automatic
verification will be presented, involving various formalisms used to
specify properties of concurrent systems. This includes specification
languages such as linear temporal logic, branching temporal logic,
process algebra and various models of automata including Buchi
automata and Asynchronous Buchi automata. The implementation of these
methods is simple and incurs only negligible overhead. An
implementation of the current version of the protocol validator SPIN
which includes partial order reductions will be described.