Cardinalities and Universal Quantifiers for Verifying Parameterized Systems
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 verification of such systems requires universally quantification to reason about parameterized state and cardinalities tracking sets of processes, messages, failures to adequately capture protocol logic. In this paper we present \Tool, an automatic invariant synthesis method that integrates cardinality-based reasoning and universal quantification. The resulting increase of expressiveness allows \Tool to verify, for the first time, a representative collection of intricate parameterized protocols.
Fri 17 JunDisplayed time zone: Tijuana, Baja California change
09:00 - 10:00
|Cardinalities and Universal Quantifiers for Verifying Parameterized Systems|
Nikolaj Bjørner Microsoft Research, Klaus Gleissenthall Technische Universität München, Andrey Rybalchenko Microsoft ResearchMedia Attached
|Ivy: Safety Verification by Interactive Generalization|
Oded Padon Tel Aviv University, Kenneth L. McMillan Microsoft Research, Aurojit Panda , Mooly Sagiv Tel Aviv University, Sharon ShohamMedia Attached