7th International workshop on Reachability Problems

      25 - 27 September 2013, Uppsala, Sweden

Foto: Othamne Rezine

Venue

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


Program

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

  Workshop:
   25 - 27 September 2013