|
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 |
|
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 |
|
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 |
|
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'') |
|
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 |
|
20:00 |
Banquet (Restaurant ``Alte Pumpe'') |
|
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 |
|
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 |
|
18:00
|
ETAPS Business Meeting |
|
9:00
ESOP invited
| Session chair: Gert Smolka (Saarland University)
Martin Odersky (EPF Lausanne)
Functional Nets |
10:00 |
Coffee |
Symbolic model-checking |
|
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) |