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

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:30 - 19:30
Concurrent and Distributed SystemsVMCAI at VMCAI
Chair(s): Dana Drachsler Cohen Technion
18:30
15m
Talk
Concurrent Correctness in Vector Space
VMCAI
Christina Peterson University of Central Florida, Victor Cook University of Central Florida, Damian Dechev University of Central Florida
Media Attached
18:45
15m
Talk
Verification of Concurrent Programs Using Petri Net Unfoldings
VMCAI
Daniel Dietsch University of Freiburg, Matthias Heizmann University of Freiburg, Germany, Dominik Klumpp University of Freiburg, Mehdi Naouar University of Freiburg, Andreas Podelski University of Freiburg, Germany, Claus Schätzle University of Freiburg
Media Attached
19:00
15m
Talk
Eliminating Message Counters in Synchronous Threshold Automata
VMCAI
Ilina Stoilkovska Vienna University of Technology , Igor Konnov Informal Systems Inc, Josef Widder Informal Systems, Florian Zuleger Vienna University of Technology
Media Attached
19:15
15m
Talk
A Reduction Theorem for Randomized Distributed Algorithms under Weak Adversaries
VMCAI
Nathalie Bertrand INRIA Rennes, Marijana Lazic Technical University of Munich, Josef Widder Informal Systems
Media Attached