Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Sun 17 Jan 2021 18:45 - 19:00 at VMCAI - Concurrent and Distributed Systems Chair(s): Dana Drachsler Cohen

We consider concurrent programs composed of a fixed number of threads over an infinite data domain. The verification of such concurrent programs requires finite state abstractions expressed through Floyd/Hoare-style assertions and it raises the problem of interleavings: each order in which the system may schedule threads has to be considered. Automatic abstraction refinement gives us techniques to find Floyd/Hoare-style assertions in software model checking. In this paper, we present a method of abstraction refinement which, given a verification problem for a concurrent program, constructs a model checking problem for a Petri net. The idea is to translate Floyd/Hoare-style assertions into synchronization constraints; by adding synchronization constraints to the Petri net, we refine the abstraction of the concurrent program through the Petri net. We solve the Petri net model checking problem via McMillan’s unfoldings which allows us to handle the large number of interleavings.

Sun 17 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:30 - 19:30
Concurrent and Distributed SystemsVMCAI at VMCAI
Chair(s): Dana Drachsler CohenTechnion
18:30
15m
Talk
Concurrent Correctness in Vector Space
VMCAI
Christina PetersonUniversity of Central Florida, Victor CookUniversity of Central Florida, Damian DechevUniversity of Central Florida
Media Attached
18:45
15m
Talk
Verification of Concurrent Programs Using Petri Net Unfoldings
VMCAI
Daniel DietschUniversity of Freiburg, Matthias HeizmannUniversity of Freiburg, Germany, Dominik KlumppUniversity of Freiburg, Mehdi NaouarUniversity of Freiburg, Andreas PodelskiUniversity of Freiburg, Germany, Claus SchätzleUniversity of Freiburg
Media Attached
19:00
15m
Talk
Eliminating Message Counters in Synchronous Threshold Automata
VMCAI
Ilina StoilkovskaVienna University of Technology , Igor KonnovInformal Systems Inc, Josef WidderInformal Systems, Florian ZulegerVienna University of Technology
Media Attached
19:15
15m
Talk
A Reduction Theorem for Randomized Distributed Algorithms under Weak Adversaries
VMCAI
Nathalie BertrandINRIA Rennes, Marijana LazicTechnical University of Munich, Josef WidderInformal Systems
Media Attached