Verification of Concurrent Programs Using Petri Net Unfoldings
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 - 18:45 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 - 19:00 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 - 19:15 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 - 19:30 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 |