Thread-Modular Model Checking

We present thread-modular model checking, a novel technique for verifying correctness properties of loosely-coupled multithreaded software systems. Thread-modular model checking verifies each thread separately using an automatically inferred environment assumption that abstracts the possible steps of other threads. Separate verification of each thread yields significant space and time savings. Suppose there are n threads, each with a local store of size L, where the threads communicate via a shared global store of size G. If each thread is finite-state (without a stack), the naive model checking algorithm requires O(G. Ln) space, whereas thread-modular model checking requires only O(n.G.(G + L)) space. If each thread has a stack, the general model checking problem is undecidable, but thread-modular model checking terminates in polynomial time.