Architecture-aware Partial Order Reduction to Accelerate Model Checking of Networked Programs

Testing cannot cover all execution schedules in concurrent software. Model checking, however, is capable of verifying the outcome of all possible executions. It has been applied successfully to networked software, with all processes being analyzed in conjunction. Unfortunately, this approach does not scale very well. This paper presents a partial-order reduction through which a performance gain of up to 70% was achieved.