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