SENVA Meeting on Parallel and Distributed Verification in collaboration with the Dutch VeriGEM project 
Scientific Programme
Monday April 3, 2006 

9h30 
Welcome – Coffee 
9h55 
Opening Jaco van de Pol (SENVA team coleader) 

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 depthfirst 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 clusterbased LTL modelchecking 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: Mucalculus 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 mucalculus
This work presents a novel gamebased approach to abstractionrefinement for the full mucalculus, interpreted over 3valued semantics. A novel notion of nonlosing strategy is introduced and exploited for refinement. Previous works on refinement in the context of 3valued semantics require a direct algorithm for solving a 3valued 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 3valued model checking game, here we reduce the problem of solving the game to solving two 2valued model checking (parity) games. In case the result is indefinite (don't know), the corresponding nonlosing strategies, when combined, hold all the information needed for refinement. This approach is beneficial since it can use any solver for 2valued 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. 

Lunch 

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
Dataflow 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 welladapted to imperative languages, it is not directly applicable to valuepassing process algebras, in which variables cannot be reset explicitly due to the singleassignment constraints of the functional programming style. This paper addresses this problem by performing dataflow 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 readonly 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 modelchecking tools. The problem is somewhat reduced by onthefly statespace reduction methods, among which PartialOrder Reduction (POR) is one of the most effective. POR yields as result a statespace 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 statespace 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 statespace 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) 
19h15 
Dinner 
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 45 different universities of the ASCI research school. (A third system, DAS3, 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 DAS2, mainly using the Ibis Javacentric middleware developed at the Vrije Universiteit. Next, the talk describes more recent experiments on a European testbed (GridLab) consisting of DAS2 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)
Abstract to be provided 
11h30 – 12h00 
Gerd Behrmann (Aalborg University) Distributed Timed Automata Reachability
Abstract to be provided 
12h00 
Lunch 

Session 6: Workshop 
13h15 – 15h00 
Draft of Future Project
Panel discussion 
15h00 – 17h00 
Technical discussions 
17h00 
Closing 