TY - CHAP
T1 - Cardinalities and universal quantifiers for verifying parameterized systems
AU - von Gleissenthal, Klaus
AU - Bjørner, Nikolaj
AU - Rybalchenko, Andrey
PY - 2016
Y1 - 2016
N2 - 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.
AB - 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.
M3 - Chapter
T3 - PLDI '16: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation
BT - Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation
PB - ACM
ER -