Preface

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:

• parallel and/or distributed-memory techniques for verification
• parallel SAT solving and its applications in verification
• I/O efficient algorithms for verification
• GPU accelerated algorithms for verification
• platform dependent verification tools
• industrial case studies employing PDMC techniques

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):

• Luboš Brim (PDMC series co-founder)
• Orna Grumberg (PDMC series co-founder)
• Kim G. Larsen
• Jaco van de Pol
• Moshe Vardi

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:

• Jiří Barnat (Masaryk University, Czech Republic) - co-chair
• Keijo Heljanko (Aalto University, Finland) - co-chair
• Henri E. Bal (Vrije University Amsterdam, Netherlands)
• Dragan Bosnacki (Eindhoven University of Technology, Netherlands)
• Luboš Brim (Masaryk University, Czech Republic)
• Gianfranco Ciardo (University of California at Riverside, US)
• Stefan Edelkamp (University of Bremen, Germany)
• John Erickson (Intel, USA)
• Youssef Hamadi (Microsoft Research, UK)
• Gerard Holzmann (NASA/JPL, USA)
• William Knottenbelt (Imperial College, UK)
• Gerald Luettgen (University of Bamberg, Germany)
• Radu Mateescu (INRIA, France)
• Jaco van de Pol (University of Twente, Netherlands)
• Michael Weber (University of Twente, Netherlands)
• Rong Zhou (Palo Alto Research Center, USA)

• Milan Ceska
• Alexander Ditter
• Alfons Laarman
• Damian Sulewski
• Siert Wieringa
• Anton Wijs
• Christoph M. Wintersteiger

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.

Distributed BDD-Based Model Checking

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:

• Image computation, in which each process computes a set of successors. This set includes both owned and non-owned states.
• Exchange, in which each process sends the non-owned states computed in the previous stage to their owners, and gets its owned states from other processes.

• T. Heyman, D. Geist, O. Grumberg, A. Schuster, "A Scalable Parallel Algorithm for Reachability Analysis of Very Large Circuits", Formal Methods in Systems Design, 21, 3, 2002.
• S. Ben-David, T. Heyman, O. Grumberg, A. Schuster, "Scalable Distributed On-the-fly Symbolic Model Checking", STTT , 2003.
• O. Grumberg, T. Heyman, A. Schuster, "Distributed Model Checking for mu-calculus", Formal Methods in System Design, 2005.
• O. Grumberg, T. Heyman, N. Ifergan, A. Schuster, "Achieving High-Speedups in Distributed Reachability Analysis through Asynchronous Computation", CHARME, 2005.
• O. Grumberg, T. Heyman, A. Schuster, "A Work-Efficient Distributed Algorithm for Reachability Analysis", Formal Methods in System Design, 2006.
• L. Fix, O. Grumberg, T. Heyman, A. Schuster, "Verifying Very Large Industrial Circuits Using 100 Processes and Beyond", Special issue of IJFCS, 2007.