Important dates:

Submission deadline:
24 May, 2012
Notification to authors:
2 July, 2012
Final version:
12 July, 2012

Submission deadline for 4-pages abstracts
August 12, 2012

Notification for 4-pages abstracts
August 19, 2012

17 - 19 September 2012


Workshop schedule


Proceedings have been published by Springer in volume 7550 of LNCS series. They are now available online at URL:


The talks will take place in the amphitheater of the LaBRI. The coffee breaks will be in room 76, on the ground floor of the LaBRI, in front of the amphitheater. Lunches (not covered by workshop fees) will take place in restaurants around the campus.


Monday, September 17, 2012

Opening and Registration
13:00-13:30 Registration
13:30-13:40 Opening
Invited Talk
13:40-14:40 Playing Games with Counter Automata
Antonin Kucera
Coffee break (14:40-15:00)
Session 1: Games
15:00-15:35 Cryptographic Protocol Verification via Supercompilation
Abdulbasit Ahmed, Alexei Lisitsa and Andrei Nemytykh
15:35-16:10 Robustness of Time Petri Nets under Guard Enlargement
S. Akshay, Loic Helouet, Claude Jard and Pierre-Alain Reynier
Coffee break (16:10-16:30)
Session 2: Sand Piles and Knots
16:30-17:05 Smooth Sand Piles
Paolo Massazza and Stefano Brocchi
17:05-17:40 On the length of knot transformations via Reidemeister
moves I and II

Rafiq Saleh

Tuesday, September 18, 2012

Invited Talk
9:25-10:25 Recursive Schemes, Krivine Machines, and Collapsible Pushdown Automata
Igor Walukiewicz
Coffee break (10:25-10:45)
Session 3: Verification
10h45-11h20 LTL-Model-Checking via Model Composition
Ingo Felscher
11:20-11:55 Well-Structured Extensions of Pushdown Systems
Xiaojuan Cai and Mizuhito Ogawa
11:55-12:30 Efficient Probabilistic Model Checking of Systems with Ranged Probabilities
Khalil Ghorbal, Parasara Sridhar Duggirala, Franjo Ivancic, Vineet Kahlon and Aarti Gupta
Lunch Break (12:30-14:15)
Invited Talk
14:15-15:15 Fraenkel-Mostowski Sets with Non-Homogeneous Atoms
Mikolaj Bojanczyk
Coffee break (15:15-15:35)
Session 4: Timed Systems
15:35-16:10 On the Relationship between Reachability Problems in Timed and Counter Automata
Christoph Haase, Joel Ouaknine and James Worrell
16:10-16:45 Ariadne: dominance checking of nonlinear hybrid automata using reachability analysis
Luca Benvenuti, Davide Bresolin, Pieter Collins, Alberto Ferrari, Luca Geretti and Tiziano Villa
16:45-17:20 Invariants for LTI Systems with Uncertain Input
Paul Hänsch and Stefan Kowalewski
Social Dinner (19:30)
19:30 - The restaurant is called Café Via Luna and is located in downtown of Bordeaux. See access map

Wednesday, September 19, 2012

Invited Talk
9:25-10:25 Decision Problems for Linear Recurrence Sequences
Joel Ouaknine
Coffee Break (10:25-10:45)
Session 5: Linear Recursions
10:45-11:20 Reachability for affine functions on the integers
Daniel Fremont
11:20-11:55 The reachability problem for vector addition systems with a stack is not elementary (paper)
Ranko Lazic
11:55-12:30 Reachable Patterns in Petri Nets
Philippe Darondeau, Stéphane Demri, Roland Meyer, and Christophe Morvan