The aim of this verification workshop is to bring together people who are interested in the development of safety and security critical systems, in formal methods in general, in automated theorem proving, and in tool support for formal developments. The overall objective of VERIFY is on the identification of open problems and the discussion of possible solutions under the theme

The emphasis of this years workshop will be on the application of formal methods to issues in computer security. Computer security is of fast-growing importance as computer systems more and more affect various aspects of everyday life. Examples are electronic commerce, computer assisted business processes, air traffic control, and multi-functional chipcards as well as databases containing personal data like, e.g., social security information, health records, or bank accounts. To ensure the security of those systems is a primordial task because security violations may endanger financial assets or even human lives. The application of formal methods during the development process results in a high confidence that the resulting systems operate correctly. Major research topics in this area are the modelling of security requirements and the development of powerful theorem proving support. Therefore, submissions in this area are especially encouraged.

Topics of interest include (but are not limited to)

Due to the focus on security of this years workshop, there are common interests with the LICS workshop on foundations of computer security, FCS. Joint submissions to both workshops are possible and, depending upon accepted papers, the two workshops will have shared sessions.

• VERIFY accepted papers
• VERIFY program
• Participant list for VERIFY

Workshop Webpage with more detailed Information

• http://www.ags.uni-sb.de/verification-ws/verify02.html

Invited speakers

• Dieter Gollmann, Microsoft Research Cambridge, UK
  joint with FCS: Defining security is difficult and error prone
• Fabio Massacci, U Trento, Italy
  joint with FCS: Formal verification of SET by Visa and Mastercard: Lessons for formal methods in security

Panel

• Ernie Cohen, Microsoft Research Cambridge, UK; Alan Jeffrey, DePaul U, USA; Fabio Martinelli, CNR Pisa, Italy; Fabio Massacci, U Trento, Italy; Catherine Meadows, Naval Research Laboratory, USA; and David Basin, U Freiburg, Germany
  joint with FCS: The future of protocol verification

Program Committee

• co-chair: Serge Autexier <autexier@dfki.de>, DFKI Saarbrücken, Germany
• co-chair: Heiko Mantel <Mantel@dfki.de>, DFKI Saarbrücken, Germany
• David Basin, U Freiburg, Germany
• Iliano Cervesato, ITT Industries, USA
• Riccardo Focardi, U Venice, Italy
• Reiner Hähnle, Chalmers U of Techn., Sweden
• Nevin Heintze, Agere Systems, USA
• Andrew Ireland, Heriot-Watt U, UK
• Deepak Kapur, U New Mexico, USA
• Christoph Kreitz, Cornell U, USA
• Fabio Martinelli, CNR Pisa, Italy
• Fabio Massacci, U Trento, Italy
• Catherine Meadows, Naval Research Laboratory, USA
• Steve Schneider, Royal Holloway, U London, UK