Cardinalities and Universal Quantifers for Verifying Parameterized Systems - , Klaus v. Gleissenthall; Bjørner, Nikolaj; Rybalchenko, Andrey (PLDI, 2016)
Parallel and distributed systems rely on intricate protocols to manage shared resources and synchronize, i.e., to manage how many processes are in a particular state. Effective veriﬁcation of such systems requires universal quantiﬁcation to reason about parameterized state and cardinalities tracking sets of processes, messages, failures to adequately capture protocol logic. In this paper we present #Π, an automatic invariant synthesis method that integrates cardinality based reasoning and universal quantiﬁcation. The resulting increase of expressiveness allows #Π to verify, for the ﬁrst time, a representative collection of intricate parameterized protocols.