Preface

The growing importance of automated formal verification in industry is driving a growing interest in those aspects that directly impact the applicability to real world problems. One of the main technical challenges lies in devising tools and techniques that allow to handle very large industrial models.

At the same time, the computer industry is undergoing a paradigm shift. Chip manufacturers are shifting development resources away from single-processor chips to a new generation of multi-processor chips, huge clusters of multi-core workstations are easily accessible everywhere, external memory devices, such as hard disks or solid state disks, are getting more powerful both in terms of capacity and access speed.

It is inevitable that verification techniques and tools need to undergo a similarly deep technological transition to catch up with the complexity of software designed for the new hardware. Recently, an increasing interest in exploiting the power of modern architectures, in particular in parallelizing and distributing verification techniques, has emerged.

The aim of the PDMC workshop series is to cover all aspects related to the verification and analysis of very large computer systems, in particular in using methods and techniques that exploit current hardware architectures. The PDMC workshop aims to provide a working forum for presenting, sharing, and discussing recent achievements in the field of high-performance verification.

The workshop included 7 regular and tool papers and the invited talk by Gianfranco Ciardo (University of California at Riverside, USA) entitled Parallel symbolic state-space exploration is difficult, but what is the alternative? Moreover, 4 workshop short presentations describing ``work in progress'' were accepted to strengthen the workshop atmosphere.

In total, out of 15 submissions 11 papers were accepted for presentation at the workshop by the following program committee:

• Henri E. Bal (Vrije University, Netherlands)
• Roberto Baldoni (University of Rome, Italy)
• Jiri Barnat (Masaryk University, Czech Republic)
• Lubos Brim (Masaryk University, Czech Republic)
• Stefan Edelkamp (University of Bremen, Germany)
• Ganesh Gopalakrishnan (University of Utah, USA)
• Keijo Heljanko (Helsinki University of Technology, Finland)
• Gerard Holzmann (JPL, USA)
• Fabrice Huet (University of Nice, France)
• William Knottenbelt (Imperial College, UK)
• Martin Leucker (TU Munchen, Germany)
• Gerald Luettgen (University of York, UK)
• Radu Mateescu (INRIA, France)
• Eric Mercer (Brigham Young University, USA)
• Jaco van de Pol (University of Twente, Netherlands)
• Cesar Sanchez (IMDEA Software, Spain)
• Maarten van Steen (Vrije University, Netherlands)

We would also like to thank the editorial board of the Electronic Proceedings in Theoretical Computer Science (EPTCS) for accepting to publish these proceedings in their series.

Lubos Brim and Jaco van de Pol
Workshop organizers and PC co-chairs