12th International Workshop on Automated Verification of Critical Systems - AVOCS 2012
18-20th September 2012
Bamberg, Germany
http://www.swt-bamberg.de/AVoCS2012/
FINAL CALL FOR PARTICIPATION
The aim of AVoCS 2012 is to contribute to the interaction and exchange of ideas among members of the
international research community working on developing tools and techniques for the verification of
critical systems.
The workshop will take place in Bamberg which is located in the Upper Franconia region of Northern
Bavaria in Germany. It is easily reachable by train from the major airports in Frankfurt and Munich and
from the regional airport in Nuremberg. Bamberg has a rich history dating back to its founding in the
10th century. The historic city center was designated a UNESCO World Heritage Site in 1993 making the
city a popular tourist destination. The city also has a reputation for producing excellent beers from its
eight local breweries, some of which we will taste in a lovely beer garden overlooking Bamberg.
The technical programme will consist of 4 invited and 16 contributed talks. The workshop will be
relatively informal, with an emphasis on discussion.
INVITED SPEAKERS
- Michael Goldsmith (U. Oxford, UK)
- Jon Holt (Atego, UK)
- Jaco van de Pol (U. Twente, NL)
- Christoph Weidenbach (MPI Informatik, Saarbruecken, D)
CONTRIBUTED TALKS
- Brijesh Dongol, John Derrick and Ian J. Hayes. Fractional Permissions and Non-Deterministic Evaluators
in Interval Temporal Logic.
- Radu I. Siminiceanu, Ijaz Ahmed and Nestor Catano. Automated Verification of Specifications with
Typestates and Access Permissions.
- Yang Zhao and Kristin Yvonne Rozier. Formal Specification and Verification of a Coordination Protocol
for an Automated Air Traffic Control System.
- Rajiv Murali and Andrew Ireland. E-SPARK: Automated Generation of Provably Correct Code from
Formally Verified Designs.
- Hassan Hatefi and Holger Hermanns. Model Checking Algorithms for Markov Automata.
- Stephan Merz and Hernán Vanzetto. Harnessing SMT Solvers for TLA+ Proofs.
- Marcel Pockrandt, Paula Herber, Holger Gross and Sabine Glesner. Optimized Transformation and
Verification of SystemC Methods.
- Holger Gast. Semi-automatic Proofs about Object Graphs in Separation Logic.
- Jeroen J.A. Keiren and Martijn D. Klabbers. Modelling and Verifying IEEE Std 11073-20601 Session
Setup Using mCRL2.
- Oleg Travkin, Heike Wehrheim and Gerhard Schellhorn. Proving Linearizability of Multiset with Local
Proof Obligations.
- Faron Moller, Hoang Nga Nguyen, Markus Roggenbach, Steve Schneider and Helen Treharne. CSP||B
Modelling for Railway Verification: The Double Junction Case Study.
- Alexander Heußner. Verifying Web Services over Unbounded, Reliable Channels.
- Abdeldjalil Boudjadar, Frits Vaandrager, Jean-Paul Bodeveix and Mamoun Filali. Callable Timed
Automata: Adding Dynamic Creation of Processes to UPPAAL.
- Maria Spichkova. Towards Focus on Time.
- Bernhard Beckert and Thorsten Bormer. Lessons Learned From Microkernel Verification.
- Adrian Beer, Uwe Kuehne, Florian Leitner-Fischer, Stefan Leue and Rüdiger Prem. Model-based Formal
Safety Analysis of an Airport Surveillance Radar System.
SPONSORED PLACEMENTS
FME Sponsored Placements: Thanks to generous sponsorship from Formal Methods Europe (FME), we are
able to offer support in the form of
several free PhD student places for those who are still registered for their PhD degrees - see
http://www.swt-bamberg.de/AVoCS2012/registration.php.
REGISTRATION
Visit our web site http://www.swt-bamberg.de/AVoCS2012/ to register. Registration will be open until
31st August 2012.
