Programme

---

September 28

Opening and Registration

• 8h45-9h35: Registration and Coffee Break
• 9h35-9h45: Opening

Invited Talk: Joost-Pieter Katoen (9h45-10h45)
Timed Automata as Observers of Stochastic Processes

Slides

Session 1:

• 10h45-11h20: Reachability and deadlocking problems in multi-stage scheduling
  Christian Eggermont and Gerhard J. Woeginger
  Slides
  
• 11h20-11h55: Lower bounds for the length of reset words in eulerian automata
  Vladimir Gusev
  Slides
  
• 11h55-12h30: A new weakly universal cellular automaton in the 3D hyperbolic space with two states
  Maurice Margenstern
  Slides
  

Lunch Break (12h30-14h00)

Invited Talk: Jean-Francois Raskin (14h00-15h00)
Reachability Problems for Hybrid Automata

Slides

Coffee Break (15h00-15h20)

Session 2:

• 15h20-15h55: Efficient Bounded Reachability Computation for Rectangular Automata
  Xin Chen, Erika Abraham and Goran Frehse
  Slides
  
• 15h55-16h30: Synthesis of Timing Parameters Satisfying Safety Properties
  Ètienne André and Romain Soulat
  Slides
  
• 16h30-17h05: Parametric Verification and Test Coverage for Hybrid Automata Using the Inverse Method
  Laurent Fribourg and Ulrich Kuehne
  Slides
  

Social Activity

Guided Tour of the Historical Center

---

September 29

Tutorial Talk: Bruno Courcelle (9h30-11)
Automata for monadic second-order model-checking

Slides

Coffee Break (11h00-11h20)

Session 3:

• 11h20-11h55: Formal Language Constrained Reachability and Model Checking Propositional Dynamic Logics
  Roland Axelsson and Martin Lange
  Slides
  
• 11h55-12h30: Characterizing Conclusive Approximations by Logical Formulae
  Yohan Boichut, Thi-Bich-Hanh Dao and Valerie Murat
  Slides
  

Lunch Break (12h30-14h00)

Session 4:

• 14h00-14h35: Completeness of the Bounded Satisfiability Problem for Constraint LTL
  Marcello M. Bersani, Achille Frigeri, Matteo Rossi and Pierluigi San Pietro
  Slides
  
• 14h35-15h10: Monotonic Abstraction for Programs with Multiply Pointed Structures
  Jonathan Cederberg, Parosh Abdulla and Tomas Vojnar

Coffee Break (15h10-15h30)

Session 5:

• 15h30-16h05: Automated Termination in Model Checking Modulo Theories
  Alessandro Carioni, Silvio Ghilardi and Silvio Ranise
  Slides
  
• 16h05-16h40: Improving Reachability Analysis of Infinite State Systems by Specialization
  Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti and Valerio Senni
  Slides
  
• 16h40-17h15: A fully symbolic bisimulation algorithm
  Malcolm Mumme and Gianfranco Ciardo
  Slides
  

Social Dinner

---

September 30

Invited Talk: Krishnendu Chatterjee (9h30-10h30)
Graph Games with Reachability Objectives: Mixing Chess, Soccer and Poker

Slides (pptx)

Coffee Break (10h30-10h50)

Session 6:

• 10h50-11h25: Decidability of LTL Model Checking for Vector Addition Systems with one zero-test
  Remi Bonnet
  Slides
  
• 11h25-12h00: Complexity Analysis of the Backward Coverability Algorithm for VASS
  Laura Bozzelli and Pierre Ganty
  Slides
  
• 12h00-12h35: Reachability for Finite-State Process Algebras Using Static Analysis
  Nataliya Skrypnyuk and Flemming Nielson
  Slides