arXiv:0912.3036v1 [cs.LO] 15 Dec 2009

DOI: 10.4204/EPTCS.14
ISSN: 2075-2180

EPTCS 14

Proceedings 8th International Workshop on
Parallel and Distributed Methods in verifiCation
Eindhoven, The Netherlands, 4th November 2009

Edited by: Lubos Brim and Jaco van de Pol

Preface
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

Preface

The 8th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2009) was held in Eindhoven, The Netherlands, on November 4, 2009, co-located with Formal Methods 2009 and other related events for the first time under the heading of Formal Methods Week.

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 wish to thank the members of the Programme Committee and also the additional reviewers for their careful evaluation of the submitted papers. We also acknowledge the effort of all members of the Programme Committee in the constructive discussion during the electronic selection meeting. Special thanks for the efforts devoted to the coordination of FMweek workshops go to Erik de Vink and Tijn Borghuis. Finally, we thank the Center of Telecommunication and Information Technology (University of Twente) for financial support.

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