Published: 31st October 2011
DOI: 10.4204/EPTCS.72
ISSN: 2075-2180


Proceedings 10th International Workshop on
Parallel and Distributed Methods in verifiCation
Snowbird, Utah, USA, July 14, 2011

Edited by: Jiří Barnat and Keijo Heljanko

Jiří Barnat and Keijo Heljanko
Invited Presentation: Platform Dependent Verification: On Engineering Verification Tools for 21st Century
Luboš Brim and Jiří Barnat
Invited Presentation: Variations on Multi-Core Nested Depth-First Search
Alfons Laarman and Jaco van de Pol
Invited Presentation: Distributed BDD-Based Model Checking
Orna Grumberg
Invited Presentation: Distributed Parametric and Statistical Model Checking
Peter Bulychev, Alexandre David, Kim Guldstrand Larsen, Marius Mikučionis and Axel Legay
Lazy Decomposition for Distributed Decision Procedures
Youssef Hamadi, Joao Marques-Silva and Christoph M. Wintersteiger
PKind: A parallel k-induction based model checker
Temesghen Kahsai and Cesare Tinelli
CoInDiVinE: Parallel Distributed Model Checker for Component-Based Systems
Nikola Beneš, Ivana Černá and Milan Křivánek
Computing Optimal Cycle Mean in Parallel on CUDA
Jiří Barnat, Petr Bauch, Luboš Brim and Milan Češka
Distributed MAP in the SpinJa Model Checker
Stefan Vijzelaar, Kees Verstoep, Wan Fokkink and Henri Bal
The HIVE Tool for Informed Swarm State Space Exploration
Anton Wijs


This volume contains the proceedings of the 10th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2011) that took place in Snowbird, Utah, on July 14, 2011. The PDMC workshop series was started by workshop that was held in Brno, Czech Republic in 2002 as a satellite event to CONCUR. Since then the PDMC workshops has been held annually as a co-located event with prestigious scientific event such as CAV (2003,2007,2011), CONCUR (2002,2004,2006), ICALP (2005), ETAPS (2008), Formal Methods (2009) and SPIN/ICGT (2010).

Originally, the PDMC series was started with the aim to provide a forum for researchers who are interested in parallel and distributed computing methods in model checking. Later on the scope was extended to cover all platform-dependent computing techniques in formal verification, hence the PDMC workshop series now covers all aspects related to the verification and analysis of very large and complex systems using, in particular, methods and techniques that exploit contemporary parallel hardware architectures. The particular topics of interest for PDMC 2011 were as follows:

To celebrate the 10th event in the series, the workshop this year included a half day invited session. The aim of the invited session was to bring together the leading scientists in the area and let them share and discuss the most important achievements in the field as well as their vision of the future. The organizers of the workshop were proud to hear ideas of the following list of excellent invited speakers and their co-authors (in alphabetic order):

For the technical half-day session, 9 submissions were reviewed by at least three members of the PDMC 2011 program committee. Two papers were accepted as full regular papers for presentations, 4 papers were accepted as innovative tool papers. The members of the program committee were as follows:

Additional reviews were carried out by the following people:

Finally, we would like to thank the local organizers Neha Rungta, Eric G Mercer, and Ganesh Gopalakrishnan for taking care of all the local arrangements. We thank the members of the Program Committee and all the additional reviewers for delivering high quality reviews. We also thank all the authors of accepted papers for their contributions, and at last, but not least, all the participants of the workshop for creating stimulating discussions. All these people contributed to quite a successful PDMC 2011 workshop.

October 2011

Jiří Barnat
Keijo Heljanko

Distributed BDD-Based Model Checking

Orna Grumberg (TECHNION - Israel Institute of Technology)

In this talk we survey a work done in the years 2000-2006 together with Tamir Heyman, Nili Ifergan, and Assaf Schuster. The goal of the work is to model check large industrial hardware designs by using the accumulative computation power and memory of a number of machines, working in parallel. We parallelize an iterative BDD-based model checking algorithm which computes the set of reachable states. Each process owns a part of the state space. The parallel algorithm works in iterations, where each iteration consists of two stages:

A significant speedup has been achieved in an asynchronous version of the algorithm, in which the image computation and the sending/receiving of owned states is done in parallel. Each process can then proceed in its own pace, without waiting for slower processes.

The work has been implemented in a tool called Division. It obtained significant memory and time reductions and could verify very large industrial hardware designs. The work stopped because SAT-based (bounded) model checking, which was faster and easier to use, has become the state-of-the-art.