Wednesday September 22, 2004

Morning

Afternoon

  9:00 -   9:25
Registration
14:00 - 14:30
A Unified Fault-Tolerance Protocol
Paul Miner, Alfons Geser, Lee Pike, and Jeffrey Maddalon
  9:25 -   9:30
Opening
14:30 - 15:00 Automating the Addition of Fail-Safe Fault-Tolerance: Beyond Fusion-Closed Specifications
Felix C. Gärtner and Arshad Jhumka
  9:30 - 10:30
Invited
speaker
Can Java really do real-time?
Greg Bollella
15:00 - 15:30 Modeling and Verification of a Fault-Tolerant Real-time Startup Protocol using Calendar Automata
Bruno Dutertre and Maria Sorea
10:30 - 10:45
Coffee break 15:30 - 15:45 Coffee break
10:45 - 11:15 Formal Verification of an avionics sensor voter using SCADE
Samar Dajani-Brown, Darren Cofer, Amar Bouali
16:00 - 16:30 Decomposing Verification of Timed I/O Automata
Dilsun Kaynar and Nancy Lynch
11:15 - 11:45 Static fault-tolerant scheduling with ``pseudo-topological'' orderings
Catalin Dima, Alain Girault, Yves Sorel
16:30 - 17:00 The Influence of Durational Actions on Time Equivalences
Harald Fecher
11:45 - 12:15 Towards a methodological Approach to Specification and Analysis of Dependable Automation Systems
Simona bernardi, Susanna Donatelli, and Giovanna Dondossola






Thursday September 23, 2004

Morning

Afternoon

  9:00 - 10:00
Invited
speaker
Of elections and electrons
Peter Ryan
14:00 - 14:30 Bounded Model Checking for Region Automata
Fang Yu, Bow-Yaw Wang and Yao-Wen Huang
10:00 - 10:15
Coffee break
14:30 - 15:00 Some Progress in Satisfiabilty Checking for Difference Logic
S. Cotton, E. Asarin, O. Maler and P. Niebert
10:15 - 10:45
On two-sided approximate model-checking: problem formulation and solution via finite topologies
J.M.Davoren, T.Moor, R.P.Gore, V.Coulthard, A.Nerode
15:00 - 15:30
Model-Checking for Weighted Timed Automata
Thomas Brihaye, Véronique Bruyère, Jean-François Raskin
10:45 - 11:15
On timed automata with input-determined guards
Deepak D'Souza and Nicolas Tabareau
15:30 - 15:45 Coffee break
11:15 - 11:45
Symbolic model checking for simply-timed systems
N. Markey and Ph. Schnoebelen
16:00 - 16:30 Symbolic Model Checking for Probabilistic Timed Automata
Marta Kwiatkowska, Gethin Norman, Jeremy Sproston and Fuzhi Wang
11:45 - 12:15
Mixed delay and threshold voters in critical real-time systems
Chiheb Kossentini and Paul Caspi
16:30 - 17:00 Structured Modeling of Concurrent Stochastic Hybrid Systems
Mikhail Bernadskiy Raman Sharykin Rajeev Alur



Conference Dinner

Friday September 24, 2004

Morning

Afternoon

  9:30 - 10:30
Invited
speaker
From Software to Hardware and Back
Paul Feautrier
14:00 - 14:30
Computing Schedules for Multithreaded Real-Time Programs using Geometry
Philippe Gerner and Thao Dang
10:30 - 10:45 Coffee break 14:30 - 15:00
Forward Reachability Analysis of Timed Petri Nets
Parosh Abdulla, Johann Deneux, Pritha Mahata and Aletta Nylen
10:45 - 11:15 Robustness and Implementability of Timed Automata
Martin De Wulf, Laurent Doyen, Nicolas Markey and Jean-Francois Raskin
15:30 - 16:00
Lazy Approximation for Dense Real-Time Systems
Maria Sorea
11:15 - 11:45 Real-time Testing with Timed Automata Testers and Coverage Criteria
Moez Krichen and Stavros Tripakis
16:00 - 16:30 Learning of Event-Recording Automata
Olga Grinchtein, Bengt Jonsson, Martin Leucker
11:45 - 12:15 Monitoring Temporal Properties of Continuous Signals
Oded Maler and Dejan Nickovic