7th International workshop on Reachability Problems

      25 - 27 September 2013, Uppsala, Sweden

Foto: Othamne Rezine


The talks will take place at Norrlands nation in the heart of central Uppsala. Lunches are covered by workshop fees.


Wednesday, September 25, 2013

Opening and Registration
8:45-9:20 Registration
9:20-9:30 Opening
Invited Talk
9:30-10:30 Reachability Modulo Theories
Shaz Qadeer
Coffee break (10:30-11:00)
Session 1
11:00-11:30 Reachability Problems for Hierarchical Piecewise Constant Derivative Systems
Paul Bell and Shang Chen
11:30-12:00 MaRDiGraS: Simplified Building of Reachability Graphs on Large Clusters
Matteo Camilli, Carlo Bellettini, Lorenzo Capra and Mattia Monga
12:00-12:30 Informal Presentation:
Kleene Algebras and Semimodules for Energy Problems
Zoltan Esik, Uli Fahrenberg, Axel Legay and Karin Quaas
Lunch Break (12:30-14:30)
Invited Talk
14:30-15:30 Robustness in Timed Automata
Patricia Bouyer-Decitre
Coffee break (15:30-16:00)
Session 2
16:00-16:30 Formal languages, word problems of groups and decidabilitys
Sam Jones and Rick Thomas
16:30-17:00 Verification of Reachability Properties for Time Petri Nets
Kais Klai, Naim Aber and Laure Petrucci
17:00-17:30 Deciding Continuous-time Metric Temporal Logic with Counting Modalities ( Slides)
Marcello M. Bersani, Matteo Rossi and Pierluigi San Pietro
17:30-18:00 Informal Presentation:
C/C++ Concurrency: Formalization and Model Finding ( Slides)
Tjark Weber

Thursday, September 26, 2013

Invited Talk
9:00-10:00 Provenance Verification
Rupak Majumdar
Coffee break (10:00-10:30)
Session 3
10:30-11:00 Completeness Results for Generalized Communication-free Petri Nets with Arbitrary Edge Multiplicities
Ernst W. Mayr and Jeremias Weihmann
11:00-11:30 Constructing Minimal Coverability Sets
Artturi Piipponen and Antti Valmari
11:30-12:00 Stable Limit Cycles for Sampled Switched Systems
Laurent Fribourg and Romain Soulat
12:00-12:30 Informal Presentation:
Validating Distributed Algorithms via Software Model Checking: Model Checking Paxos in SPIN
Giorgio Delzanno
Lunch Break (12:30-14:30)
Invited Talk
14:30-15:30 Automated Verification of Concurrent Software
Daniel Kroening
Coffee break (15:30-16:00)
Session 4
16:00-16:30 Parameterized Verification of Broadcast Networks of Register Automata
Giorgio Delzanno, Arnaud Sangnier and Riccardo Traverso
16:30-17:00 Branching-Time Model Checking Gap-Order Constraint Systems
Richard Mayr and Patrick Totzke
17:00-17:30 Parametric Interrupt Timed Automata
Beatrice Berard, Serge Haddad, Aleksandra Jovanovic and Didier Lime
Dinner at Peppar Peppar (19.30)

Friday, September 27, 2013

Invited Talk
9:00-10:00 The dynamic complexity of the reachability problem on graphs
Thomas Schwentick
Coffee break (10:00-10:30)
Session 5
10:30-11:00 Modular Synthesis with Open Components
Ilaria De Crescenzo and Salvatore La Torre
11:00-11:30 On The Complexity of Counter Reachability Games ( Slides)
Julien Reichert
11:30-12:00 Monomial Strategies for Concurrent Reachability Games and Other Stochastic Games
Soren Kristoffer Stiil Frederiksen and Peter Bro Miltersen
12:00-12:30 Informal Presentation:
Reachability problems for Braids
Igor Potapov
Lunch Break (12:30-14:00)

Uppsala University

  Important dates:

  Submission deadline
  for 4-pages abstracts:
  12 August 2013

  Notification to authors
  for 4-pages abstracts::
  19 August 2013

   25 - 27 September 2013