Programme for AVoCS'04
----------------------

9:00-10:00 Invited Talk
Extracting Algorithms from Code.
Georges Gonthier, Microsoft Research (UK).

10:00-10:15 Software Model Checking Based on Game Semantics and CSP
Aleksandar Dimovski and Ranko Lazic.

10:15-10:30 Model-checking the Preservation of Temporal Properties upon Feature Integration
Dimitar P. Guelev, Mark Ryan, and Pierre Yves Schobbens.


10:30-11:00 Break


11:00-11:20 Formal Verification of the NASA Runway Safety Monitor
Radu I. Siminiceanu and Gianfranco Ciardo.

11:20-11:40 Regularity results for FIFO channels
Nils Klarlund and Richard Trefler.

11:40-12:00 Simplifying Itai-Rodeh Leader Election for Anonymous Rings
Wan Fokkink and Jun Pang.

12:00-12:15 About Fast and TReX accelerations
Christophe Darlot, Alain Finkel, and Laurent van Begin.

12:15-12:30 Probabilistic Model Checking of the CSMA/CD protocol using PRISM and APMC
Marie Duflot, Laurent Fribourg, Thomas Herault, Richard Lassaigne,
Frederic Magniette, Stephane Messika, Sylvain Peyronnet, and Claudine Picaronny.

12:30-12:45 Structural Translation from Time Petri Nets to Timed Automata
Franck Cassez and Olivier-H. Roux.

12:45-13:00 CTL-Property transformations along an incremental design process
Cecile Braunstein and Emmanuelle Encrenaz.


13:00-14:30 Lunch and PC meeting


14:30-14:50 True Concurrent Logic via In-Between Specification
Harald Fecher.

14:50-15:10 Toward a Small Model Theorem for Data Independent Systems in Alloy
Lee Momtahan.

15:10-15:30 Efficient Model Checking of Hardware Using Conditioned Slicing
Shobha Vasudevan, E. A. Emerson, and Jacob A. Abraham.

15:30-15:45 Finding symmetry in models of concurrent systems by static channel diagram analysis
Alastair Donaldson, Alice Miller, and Muffy Calder.

15:45-16:00 A generic cost model for concurrent and data-parallel meta-computing
Armelle Merlin and Gaetan Hains.


16:00-16:30 Break


16:30-16:50 Games for Counting Abstractions
Jean-Francois Raskin, Mathias Samuelides, and Laurent Van Begin.

16:50-17:10 Towards a unifying CSP approach for hierarchical verification of asynchronous hardware
X. Wang, M. Kwiatkowska, G. Theodoropoulos, and Q. Zhang.

17:10-17:30 Model Checking Functional and Performability Properties of Stochastic Fluid Models
Marco Gribaudo and Andras Horvath.

17:30-17:45 Combining the box structure development method and CSP for industrial software development
Philippa J. Hopcroft and Guy H. Broadfoot.

17:45-18:00 Finding Extremal Models of Discrete Duration Calculus formulae using Symbolic Search
Paritosh K. Pandya.

18:00 Closing and End