September 11, 2020
In this talk, we present (aspects of) our project, Discover[i], which aims to support fully-automated parameterized verification of distributed systems, i.e., verification of systems instantiated with an arbitrary number of processes. First, we present the GSP model, a new computational model for parameterized systems that are based on a general global synchronization primitive and allows for global transition guards. We show that reachability properties are decidable for a large class of systems in the GSP model. Furthermore, we provide sufficient conditions for small cutoffs. Second, building on the theoretical results of the GSP model, we develop a framework, QuickSilver, for modeling and automated parameterized reasoning about systems that build on distributed agreement protocols, such as consensus or leader election.