Methods to Model-Check Parallel Systems Software

Olga Shumsky Matlin, William McCune, Ewing Lusk

We report on an effort to develop methodologies for formal verification of parts of the Multi-Purpose Daemon (MPD) parallel process management system. MPD is a distributed collecti…