Doron Peled

AT&T Bell Labs

Efficient model-checking using partial order reductions

DIMACS Center - Room 431
Busch Campus
Piscataway, New Jersey
October 11, 1995 at 4:30 PM


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.