Published: 15th December 2009|
|Parallel symbolic state-space exploration is difficult, but what is the alternative? Gianfranco Ciardo, Yang Zhao and Xiaoqing Jin||1|
|Formal Aspects of Grid Brokering Attila Kertész and Zsolt Németh||18|
|Distributed Branching Bisimulation Minimization by Inductive Signatures Stefan Blom and Jaco van de Pol||32|
|Efficient Parallel Statistical Model Checking of Biochemical Networks Paolo Ballarini, Michele Forlin, Tommaso Mazza and Davide Prandi||47|
|Tarmo: A Framework for Parallelized Bounded Model Checking Siert Wieringa, Matti Niemenmaa and Keijo Heljanko||62|
|An Efficient Explicit-time Description Method for Timed Model Checking Hao Wang and Wendy MacCaull||77|
|Parallelizing Deadlock Resolution in Symbolic Synthesis of Distributed Programs Fuad Abujarad, Borzoo Bonakdarpour and Sandeep S. Kulkarni||92|
|DiVinE-CUDA - A Tool for GPU Accelerated LTL Model Checking Jiří Barnat, Luboš Brim and Milan Češka||107|
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:
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