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 |
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) |
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) |