Fri 17 Jun 2016 09:00 - 09:30 at Grand Ballroom San Rafael - Verification II Chair(s): Armando Solar-Lezama

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 Jun
Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change

09:00 - 10:00: Research Papers - Verification II at Grand Ballroom San Rafael
Chair(s): Armando Solar-LezamaMIT
pldi-2016-papers09:00 - 09:30
Nikolaj BjørnerMicrosoft Research, Klaus GleissenthallTechnische Universität München, Andrey RybalchenkoMicrosoft Research
Media Attached
pldi-2016-papers09:30 - 10:00
Oded PadonTel Aviv University, Kenneth L. McMillanMicrosoft Research, Aurojit Panda, Mooly SagivTel Aviv University, Sharon Shoham
Media Attached