SENVA Meeting on Parallel and

Distributed Verification
CWI (Amsterdam, The  Netherlands)

in collaboration with the Dutch VeriGEM project



Scientific Programme

Monday April 3, 2006


Welcome – Coffee



Jaco van de Pol (SENVA team co-leader)


Session 1: Distributed Model Checking

Chair: Jaco van de Pol

10h00 – 10h45

Radu Mateescu (SENVA) – Joint work with Christophe Joubert

Sequential and Distributed Test Generation using Boolean Equation Systems


Conformance test generation based on verification techniques as implemented in the TGV tool proved its practical usefulness for analysing industrial systems. However, the underlying state space exploration algorithms are based upon depth-first search traversals and therefore unsuitable for distribution. We propose an encoding of the test generation problem as the local resolution with diagnostic of a boolean equation system (BES). This enables to use transparently the sequential and distributed BES resolution algorithms provided by the CAESAR_SOLVE library of CADP for generating conformance test cases on the fly. This method was implemented in a prototype tool named EXTRACTOR, and preliminary experiments show that this approach compares favourably with TGV in terms of memory consumption.

10h45 – 11h20

Ivana Cerna (Masaryk University Brno) joint work with Jiri Barnat  and Lubos Brim

Distributed LTL Model Checking of Probabilistic Systems


A technique for cluster-based LTL model-checking of finite Markov decision processes is presented. The approach builds on the detection of presence of accepting ergodic sets using reversed OWCTY state elimination technique.


Coffee Break


Session 2: Mu-calculus and Boolean Equation Systems

Chair: Lubos Brim

11h35 12h30

Martin Leucker (Technical University of Muenchen) – joint work with Orna Grumberg, Martin Lange, and Sharon Shoham

Don't know in the mu-calculus


This work presents a novel game-based approach to abstraction-refinement for the full mu-calculus, interpreted over 3-valued semantics. A novel notion of non-losing strategy is introduced and exploited for refinement. Previous works on refinement in the context of 3-valued semantics require a direct algorithm for solving a 3-valued model checking game. This was necessary in order to have the information needed for refinement available on one game board. In contrast, while still considering a 3-valued model checking game, here we reduce the problem of solving the game to solving two 2-valued model checking (parity) games. In case the result is indefinite (don't know), the corresponding non-losing strategies, when combined, hold all the information needed for refinement. This approach is beneficial since it can use any solver for 2-valued parity games. Thus, it can take advantage of newly developed such algorithms with improved complexity or by distributed model checkers.

12h30 – 13h10

Jan Friso Groote (Technical University of Eindhoven) – joint work with Kaļs Klaļ

A framework for parameterised Boolean equations


Boolean Equation Systems (BESs) have gained popularity as it is a very natural system to which model checking questions can be translated. The question of whether a modal formula holds on a transition system reduces to the question whether a boolean variable in a BES has the value true.  We are modelling and analysing real systems. In order to do so, we absolutely need data types. Within the process domain we do the large part of the analysis of the behaviour of processes in the data domain. When encountering modal formulas in the domain of real systems, we cannot do without data. But this means that our Boolean Equation Systems also need data. So, following Mateescu (1998) we are looking at Parameterised Boolean Equation Systems (PBESs). In this presentation we show that PBESs can be solved by data manipulation and we explain that we are currently working on a toolset that assists in helping solving PBESs with data manipulations.




Session 3: State Space Reduction

Chair: Jan Friso Groote

14h15 – 15h00

Hubert Garavel (SENVA) – joint work with Wendelin Serwe

State Space Reduction for Process Algebra Specifications


Data-flow analysis to identify ``dead'' variables and reset them to an ``undefined'' value is an effective technique for fighting state explosion in the enumerative verification of concurrent systems. Although this technique is well-adapted to imperative languages, it is not directly applicable to value-passing process algebras, in which variables cannot be reset explicitly due to the single-assignment constraints of the functional programming style. This paper addresses this problem by performing data-flow analysis on an intermediate model (Petri nets extended with state variables) into which process algebra specifications can be translated automatically. It also addresses important issues, such as avoiding the introduction of useless reset operations and handling shared read-only variables that children processes inherit from their parents.

15h00 –15h30

Michael Weber (SENVA)

Static Analyses for State Space Reduction


The state space explosion problem is still the limiting factor for the applicability of model-checking tools.  The problem is somewhat reduced by on-the-fly state-space reduction methods, among which Partial-Order Reduction (POR) is one of the most effective.  POR yields as result a state-space which is smaller, but indistinguishable under a temporal logic specification from the unreduced one.  However, POR techniques so far are highly language dependant, and usually tightly integrated with state-space generators.  Additionally, they do not work equally well in all settings, for example in distributed state space generation. To counter these restrictions, we present an extended version of a static analysis called Path Reduction by Yorav and Grumberg, which is only dependant on an intermediate representation, and does not require changes in the state-space generator, nor the compiler generating the intermediate representation.  The reduction preserves CTL*-X properties, and performs well in practice.


Coffee Break


Session 4: Position Statements on Future Project

Chair: Jaco van de Pol

16h00 – …

Grenoble – Hubert Garavel (SENVA)

Brno – Lubos Brim (Masaryk University Brno)

Eindhoven – Jan Friso Groote (Technical University of Eindhoven)

Muenchen – Martin Leucker (Technical University of Muenchen)

Twente – Matthias Kuntz (University of Twente)

Aalborg – Gerd Behrmann (University of Aalborg)

… – 18h00

Amsterdam – Jaco van de Pol (SENVA)



Tuesday April 4, 2006


Session 5: Grids

Chair: Radu Mateescu

9h30 10h30

Henri Bal (Vrije Universiteit Amsterdam)

Distributed supercomputing on DAS, GridLab, and Grid'5000


The Distributed ASCI Supercomputer (DAS) is an infrastructure for experimental computer science research on distributed systems and grids. Two DAS systems have been built so far, each consisting of multiple Myrinet clusters located at 4-5 different universities of the ASCI research school. (A third system, DAS-3, is under way.) This talk first summarizes the history of DAS and describes its impact on Dutch computer science research. Next, it discusses distributed supercomputing experiments on DAS-2, mainly using the Ibis Java-centric middleware developed at the Vrije Universiteit. Next, the talk describes more recent experiments on a European testbed (GridLab) consisting of DAS-2 and other clusters, and on the French Grid'5000 system.


Short Coffee Break

10h40 – 11h05

Open discussion with Henri Bal

11h05 – 11h30

Josva Kleist (Aalborg University)

What is a Grid?


Abstract to be provided

11h30 – 12h00

Gerd Behrmann (Aalborg University)

Distributed Timed Automata Reachability


Abstract to be provided




Session 6: Workshop

13h15 – 15h00

 Draft of Future Project


Panel discussion

15h00 – 17h00

Technical discussions