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.