Parameterized verification of π-calculus systems

In this paper we present an automatic verification technique for parameterized systems where the subsystem behavior is modeled using the π-calculus. At its core, our technique treats each process instance in a system as a property transformer. Given a property φ that we want to verify of an N-process system, we use a partial model checker to infer the property φ′ (stated as a formula in a sufficiently rich logic) that must hold of an (N - 1)-process system. If the sequence of formulas φ, φ′, . . . thus constructed converges, and the limit is satisfied by the deadlocked process, we can conclude that the N-process system satisfies φ. To this end, we develop a partial model checker for the π-calculus that uses an expressive value-passing logic as the property language. We also develop a number of optimizations to make the model checker efficient enough for routine use, and a light-weight widening operator to accelerate convergence. We demonstrate the effectiveness of our technique by using it to verify properties of a wide variety of parameterized systems that are beyond the reach of existing techniques.