6th International Workshop on Automated Verification of Critical Systems

LORIA Nancy, France


All talks will be held at LORIA. Lunches will take place at the LORIA cafeteria.

The guided tour of Nancy on Monday evening will start at the tourist office which is located at Place Stanislas in the city center. The workshop dinner will be at the restaurant "Le Grand Café Foy" at Place Stanislas.

Abstracts and documents of all contributions are available at http://hal.inria.fr/AVOCS06.


Monday, 18 September 2006

9.00

Opening

Invited talk

9.15

Byron Cook
Automatic termination proofs for software

10.15

Coffee break

Contributed talks

10.45

Jean-Paul Bodeveix, Mamoun Filali, Julia Lawall and Gilles Muller
Automatic Verification of Bossa Scheduler Properties

11.15

Dominique Cansell and Dominique Méry
Incremental Parametric Development of Greedy Algorithms

11.45

Frank Ortmeier and Gerhard Schellhorn
Formal Fault Tree Analysis: Practical Experiences

12.30

Lunch

Invited talk

14.00

Oded Maler
Fighting the Clocks Explosion

Contributed talks

15.00

Michaël Cadilhac, Thomas Hérault, Richard Lassaigne, Sylvain Peyronnet and Sébastien Tixeuil
Evaluating complex MAC protocols for sensor networks with APMC

15.30

Lars-Henrik Eriksson
The GTO Toolset and Method

16.00

Coffee break

Short presentations

16.30

Joris Rehm
A method to refine time constraints in event B framework

16.45

Clément Hurlin
Proof reconstruction for first-order logic and set-theoretical constructions

17.00

David Déharbe and Pascal Fontaine
haRVey: combining reasoners

17.15

Bo Zhang
On the Formal Verification of the FlexRay Communication Protocol

Evening Activities

18.30

Tour of Nancy

20.00

Workshop dinner

 

Tuesday, 19 September 2006

Invited talk

9.00

Véronique Cortier
Verification of cryptographic protocols: techniques and link to cryptanalysis

10.00

Coffee break

Contributed talks

10.30

Alastair F. Donaldson and Alice Miller
Extending Symmetry Reduction Techniques to a Realistic Model of Computation

11.00

Nick Moffat and Michael Goldsmith
Assumption-Commitment Support for CSP Model Checking

11.30

Sara Gradara, Antonella Santone and Maria Luisa Villani
Formal Verification of Concurrent Systems via Directed Model Checking

12.15

Lunch

Invited talk

13.30

Bill Roscoe
The past, present and future of protocol checking with CSP and FDR

Contributed talks

14.30

Eldar Kleiner and Tom Newcomb
On the Decidability of the Safety Problem for Access Control Policies

15.00

Hasan Amjad
Compressing Propositional Refutations

15.30

Coffee break

Short presentations

16.00

Martin Strecker and Mathieu Giorgino
Towards a Formalisation of Graph Transformations in Proof Assistants

16.15

Maik Kollmann and Yuen Man Hon
Multi-Object Checking Counterexamples

16.30

Yuen Man Hon and Maik Kollmann
Simulation and Verification of UML-based Railway Interlocking Designs

16.45

Charu Arora and Mathieu Turuani
Adding Integrity to the Ephemerizer's Protocol

End of workshop