Preface Electronic Communications of the EASST Volume 23 (2009) Proceedings of the Ninth International Workshop on Automated Verification of Critical Systems (AVOCS 2009) Preface Markus Roggenbach 2 pages Guest Editor: Markus Roggenbach Managing Editors: Tiziana Margaria, Julia Padberg, Gabriele Taentzer ECEASST Home Page: http://www.easst.org/eceasst/ ISSN 1863-2122 http://www.easst.org/eceasst/ ECEASST Preface AVOCS, the workshop on Automated Verification of Critical Systems, is an annual meeting that brings together researchers and practitioners to exchange new results on tools and tech- niques for the verification of critical systems. Topics of interest cover all aspects of automated verification, including model checking, theorem proving, abstract interpretation, and refinement pertaining to various types of critical systems (safety-critical, security-critical, business-critical, performance-critical, etc.). Contributions that describe different techniques, or industrial case studies are encouraged. This volume contains the proceedings of the ninth workshop on Automated Verification of Critical Systems (see also http://www.cs.swan.ac.uk/avocs09/), which was hosted by Swansea University, Wales, UK, and which took place during September 23–25, 2009, at the conference centre Gregynog. Previous AVOCS workshops were held at the University of Oxford (2001 and 2007), the University of Birmingham (2002), the University of Southampton (2003), the Royal Society in London (2004), the University of Warwick (2005), LORIA, Nancy (2006), and the University of Glasgow (2008). AVOCS 2010 will take place in Düsseldorf, Germany. In 2009 authors from twelve countries, namely from Algeria, Egypt, Estonia, France, Ger- many, India, Italy, Japan, The Netherlands, Portugal, the United Kingdom, and the United States, submitted papers to AVOCS. AVOCS 2009 received 17 submissions for Full Papers, out of which 12 were selected for presentation at the workshop. Furthermore, AVOCS received 10 submissions for Short Con- tributions all of which were accepted. The selection process was carried out by the Program Committee, taking into account the originality, quality, and relevance of the material presented in each submission. The selected and revised Full Papers are included in this volume, together with the contributions from the invited speakers Ulrich Berger and Christoph Lüth. 1 / 2 Volume 23 (2009) http://www.cs.swan.ac.uk/avocs09/ Preface I wish to thank all authors who submitted their papers to AVOCS 2009, Erwin R. Catesbeiana (Jr) for help with workshop organization on the fly, the Program Committee for its excellent work, the reviewers who supported the Program Committee in the evaluation and selection pro- cess, and Phillip James, Temesghen Kahsai, and Liam O’Reilly for the local organization. I am grateful to the Department of Computer Science at Swansea University for hosting the event and thank IT Wales for sponsoring AVOCS 2009. AVOCS 2009 gratefully acknowledges the excellent cooperation with the Conference Centre Gregynog and the use of EasyChair, the conference management system by Andrei Voronkov. Swansea, December 2009 Markus Roggenbach AVOCS 2009 Program Committee David Aspinall University of Edinburgh, Scotland, UK Muffy Calder University of Glasgow, Scotland, UK Michael Goldsmith University of Warwick, UK Constance Heitmeyer Naval Research Laboratory, Washington DC, USA Gerald Luettgen University of Bamberg, Germany Eric Mercer Brigham Young University, Utah, USA Stephan Merz INRIA, Nancy, France Alice Miller University of Glasgow, Scotland, UK Paritosh Pandya IIT Mumbai, India Silvio Ranise University of Verona, Italy Markus Roggenbach (Chair) Swansea University, Wales, UK Bill Roscoe University of Oxford, UK Mark Ryan University of Birmingham, UK Helen Treharne University of Surrey, UK Markus Wenzel TU München, Germany Sergio Yovine Verimag, France AVOCS 2009 Reviewers Arnold Beckmann Swansea University, Wales, UK Ulrich Berger Swansea University, Wales, UK Jan Calta Humboldt University Berlin, Germany Jean-Christophe Filliatre Université Paris Sud, France Dominique Mery INRIA, Nancy, France Jan Tobias Muehlberg University of Bamberg, Germany Dirk Pattinson Imperial College London, UK Heiko Schmidt University of Bamberg, Germany Stefano Tonetta FBK-Irst, Italy Edward Turner University of Surrey, UK Dennis Walter Bremen University, Germany David Williams University of Surrey, UK Proc. AVOCS 2009 2 / 2