Clicking on day shows daily programme, clicking on name shows the authors list, clicking on room number shows location plan.

Monday, March 27
9:00
Opening
Session chair: Bernd Mahr (TU Berlin)
9:30

FOSSACS
invited

Session chair: Jerzy Tiuryn (Warsaw University)

Abbas Edalat (Imperial College, London)
A Data Type for Computational Geometry and Solid Modelling

Software and Formal methods tools
Session chair: Susanne Graf (VERIMAG, Grenoble)
14:00 An extensible type system for component-based design
Yuhong Xiong, Edward A. Lee (UC Berkely)
D
E
M
O
S
14:30 Proof General: a generic tool for proof development
David Aspinall (University of Edinburgh)
15:00 ViewPoint-oriented software development: tool support for integrating multiple perspectives by distributed graph transformation
Michael Goedicke, Thorsten Meyer, Bettina Enders (University of Essen), Gabriele Taentzer (TU Berlin)
15:30 Coffee
Formal methods tools
Session chair: Perdita Stevens (University of Edinburgh)
16:00 Consistent integration of formal methods (tool)
Peter Braun, Heiko Lötzbeyer, Bernhard Schätz, Oscar Slotosch (TU München)
16:30 An architecture for interactive program provers (tool)
Jörg Meyer, Arnd Poetzsch-Heffter (FernUni Hagen)
17:00 The PROSPER toolkit
Louise A. Dennis, Graham Collins, Graham Robinson, Tom Melham (University of Glagow), Michael Norrish, Konrad Slind, Mike Gordon (University of Cambridge), Richard Boulton (University of Edinburgh)
17:30 CASL: from semantics to tools
Till Mossakowski (University of Bremen)
18:00 Coffee
18:30

GRATRA
invited

Session chair: Hartmut Ehrig (TU Berlin, Germany)

Grzegorz Rozenberg (Universiteit Leiden, Netherlands)
DNA Computing in Vivo and Graph Transformation

Tuesday, March 28
9:00

FASE
invited

Session chair: Tom Maibaum (King's College London)

Wlad Turski (University of Warsaw, Poland)
An Essay on Software Engineering at the Turn of Century

10:00 Coffee
Timed and hybrid systems
Session chair: Ed Brinksma (University of Twente)
10:30 On the construction of live timed systems
Sébastien Bornot, Gregor Gößler, Joseph Sifakis (VERIMAG, Grenoble)
11:00 On memory-block traversal problems in model-checking timed systems
Fredrik Larsson, Paul Pettersson, Wang Yi (Uppsala University)
11:30 Symbolic model checking for rectangular hybrid systems
Thomas A. Henzinger, Rupak Majumdar (UC Berkeley)
12:00 Efficient data structure for fully symbolic verification of real time software systems
Farn Wang (Academia Sinica)
12:30 Lunch
14:00

Panel
Standard Components off the Shelf -
Do they carry and need a (Formal) Standard Semantics?

Chair: Herbert Weber (TU Berlin)
Participants: Christine Choppy, Werner Damm, Hartmut Ehrig, José Luiz Fiadeiro, Bernd Mahr, Richard M. Soley
18:30 Reception (TU-``Lichthof'')
Wednesday, March 29
9:00

ETAPS
invited

Session chair: Bernd Mahr (TU Berlin)

Richard M. Soley
(OMG Object Management Group)
Memex isn't Enough

10:00 Coffee
Infinite and parameterized systems
Session chair: Michael I. Schwartzbach (BRICS, University of Aarhus)
10:30 Verification of parameterized systems using logic-program transformations
Abhik Roychoudhury, K. Narayan Kumar, C.R. Ramakrishnan, I.V. Ramakrishnan, Scott A. Smolka (SUNY at Stony Brook)
11:00 Abstracting WS1S systems to verify parameterized networks
Kai Baukus, Karsten Stahl (University of Kiel), Saddek Bensalem, Yassine Lakhnech (VERIMAG, Grenoble)
11:30 FMona: a tool for expressing validation techniques over infinite state systems
Jean-Paul Bodeveix, Mamoun Filali (IRIT, Toulouse)
12:00 Transitive closures of regular relations for verifying infinite state systems
Bengt Jonsson, Marcus Nilsson (Uppsala University)
12:30 Lunch
14:30

ETAPS
invited

Session chair: Don Sannella (University of Edinburgh)

David Harel
(The Weizmann Institute of Science)
From Play-In Scenarios to Code: an Achievable Dream

15:30 Coffee
Diagnostic and test generation
Session chair: Claude Jard (IRISA, Rennes)
17:00 Using static analysis to improve automatic test generation
Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu (VERIMAG, Grenoble)
17:30 Efficient diagnostic generation for boolean equation systems
Radu Mateescu (INRIA, Rhône-Alpes)
20:00 Banquet (Restaurant ``Alte Pumpe'')
Thursday, March 30
9:00

TACAS
invited

Session chair: Susanne Graf (VERIMAG, Grenoble)

Pierre Wolper (University of Liège)
On the Representation of Constraints by Automata in the Verification of Infinite Systems

10:00 Coffee
Efficient model-checking
Session chair: Wang Yi (Uppsala University)
10:30 Compositional state space generation with partial order reductions for asynchronous communicating systems
Jean-Pierre Krimm, Laurent Mounier (VERIMAG, Grenoble)
11:00 Checking for CFFD-preorder with tester processes
Juhana Helovuo, Antti Valmari (Tampere University of Technology)
11:30 Fair bisimulation
Thomas A. Henzinger (UC Berkeley), Sriram K. Rajamani (Microsoft Research)
12:00 Integrating low level symmetries into reachability analysis
Karsten Schmidt (HU Berlin)
12:30 Lunch
14:30

CC
invited

Session chair: David Watt (University of Glasgow)

Reinhard Wilhelm (Universität des Saarlandes)
Shape Analysis

15:30 Coffee
Model-checking tools
Session chair: Constance L. Heitmeyer (Naval Research, Washington)
16:00 Model checking for the ASM high level language
Giuseppe del Castillo (University of Paderborn), Kirsten Winter (GMD Berlin)
16:30 A Markov chain model checker
Holger Hermanns, Joost-Pieter Katoen (University of Twente), Joachim Meyer-Kayser, Markus Siegle (University of Erlangen-Nürnberg)
17:00 Model checking SDL with Spin
Dragan Bosnacki, Dennis Dams, Leszek Holenderski, Natalia Sidorova (TU Eindhoven)
17:30 Salsa: combining constraint solvers with BDDs for automatic invariant checking
Ramesh Bharadwaj (Naval Research Lab), Steve Sims (SUNY Stony Brook)
18:00

ETAPS Business Meeting
Friday, March 31
9:00

ESOP
invited

Session chair: Gert Smolka (Saarland University)

Martin Odersky (EPF Lausanne)
Functional Nets

10:00 Coffee
Symbolic model-checking
Session chair: Perdita Stevens (University of Edinburgh)
10:30 Symbolic model checking of probabilistic processes using MTBDDs and the Kronecker representation
Luca de Alfaro (UC Berkeley), Marta Kwiatkowska, Gethin Norman, David Parker (University of Birmingham), Roberto Segala (University of Bologna)
11:00 Symbolic reachability analysis based on SAT solvers
Parosh Aziz Abdulla (Uppsala University), Per Bjesse, Niklas Eén (Chalmers University of Technology)
11:30 Symbolic representation of upward-closed sets
G. Delzanno (MPI Saarbrücken), J.-F. Raskin (UC Berkeley)
12:00 BDD vs. constraint-based model checking: an experimental evaluation for asynchronous concurrent systems
Tevfik Bultan (UC Sanat Barbara)
12:30 Lunch
Visual tools
Session chair: Michael I. Schwartzbach (BRICS, University of Aarhus)
14:30 Tool-based specification of visual languages and graphic editors
Magnus Niemann, Roswitha Bardohl (TU Berlin)
15:00 VIP: a visual editor and compiler for v-Promela
Moataz Kamel (University of Waterloo, Canada), Stefan Leue (University of Freiburg, Germany)
15:30 Coffee
Verification of critical systems
Session chair: Claude Jard (IRISA, Rennes)
16:00 A comparison of two verification methods for speculative instruction execution
Tamarah Arons, Amir Pnueli (The Weizmann Institute of Science)
16:30 Partial order reductions for security protocol verification
Edmund Clarke, Somesh Jha, Will Marrero (Carnegie Mellon University)
17:00 Model checking security protocols using a logic of belief
Massimo Benerecetti, Fausto Giunchiglia (University of Trento)
17:30 A formal specification and validation of a critical system in presence of byzantine errors
S. Gnesi, D. Latella, G. Lenzini (CNR, Pisa), C. Abbaneo, A. Amendola, P. Marmo (Ansaldo, Genova)
18:00
Closing
Session chair: Bernd Mahr (TU Berlin)

Information maintained by Doris Fähndrich