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)