[Om-announce] Call for participation: VERIFY'06

[Serge Autexier]

[Apologies if your receive multiple copies]
[Early registration deadline: Monday, 10 July 2006]

		        CALL FOR PARTICIPATION

	  3rd International Verification Workshop (VERIFY'06)

 What are the verification problems? What are the deduction techniques?

		 in connection with IJCAR'06 at FLoC'06

		    August 15-16, 2006, Seattle, USA

            [http://www.easychair.org/FLoC-06/VERIFY.html]

The formal verification of   critical information systems has  a  long
tradition as   one  of the  main  areas of  application for  automated
theorem  proving.    Nevertheless,  the  area  is  of  still   growing
importance as the number of computers affecting  everyday life and the
complexity of  these systems are both increasing.   The purpose of the
VERIFY workshop  series is to  discuss   problems arising  during  the
formal  modeling   and  verification  of  information systems  and  to
investigate suitable solutions.   Possible  perspectives include those
of automated theorem  proving,  tool support, system  engineering, and
applications.

The   VERIFY   workshops  aim  at  bringing  together  people  who are
interested in the development of safety and security critical systems,
in formal  methods, in the  development  of automated theorem  proving
techniques, and  in  the  development  of  tool   support.   Practical
experiences  gained in realistic verifications  are of interest to the
automated theorem proving community and new theorem proving techniques
should be transferred into   practice.  The overall objective  of  the
VERIFY workshops is to identify open problems  and to discuss possible
solutions under the theme

What are the verification problems? What are the deduction techniques?

In  2006,   VERIFY will  specifically   consider issues  regarding the
application of "tool support   for formal modeling,  verification  and
stepwise  system  development" without excluding submissions regarding
other topics in the focus of the  workshop.  Therefore, submissions in
this area are especially encouraged.


KEYNOTE SPEAKERS

* John Rushby  (SRI International)
  Threatened by a Great Opportunity: Disruptive Innovation in Formal
  Verification

* Luca Vigano  (ETH Zürich)
  Automated Reasoning for Security Protocol Analysis

* Christoph Walther  (TU Darmstadt)
  Verification in the Classroom


ACCEPTED PAPERS

* Robert Palmer, Ganesh Gopalakrishnan, and Mike Kirby
  Formal Specification and Verification Using +CAL: An Experience
  Report

* Viorica Sofronie-Stokkermans
  Local reasoning in verification

* Laura Ildiko Kovacs, Tudor Jebelean
  Finding Polynomial Invariants for Imperative Loops in the Theorema
  System

* Bernhard Beckert, Vladimir Klebanov
  Must Program Verification Systems and Calculi be Verified?

* Dieter Hutter
  Automating Proofs of Unwinding Conditions

* Andreas Schlosser, Christoph Walther, and Markus Aderhold
  Axiomatic Specifications in VeriFun

* Achim D. Brucker, Burkhart Wolff
  A Package for Extensible Object-Oriented Data Models with an
  Application to IMP++

* Sara Van Langenhove, Albert Hoogewijs
  Verifying Sliced Hierarchical Statecharts with SVtL

* Siraj Shaikh, Vicky Bush, and Steve Schneider
  A heuristic for constructing rank functions to verify authentication
  protocols

* Raghavendra Kagalavadi Ramesh, Deepak D'Souza
  Checking Unwinding Conditions for Finite State Systems

* Myla Archer, Elizabeth Leonard
  Establishing High Confidence in Code Implementations of Algorithms
  using Formal Verification of Pseudocode

	
The registration for the workshop is via the FLOC'06 registration
webpage:

     http://www.easychair.org/FLoC-06/floc-registration.html

We are looking forward to see you at the workshop!

Serge Autexier & Heiko Mantel

-- 
Serge Autexier                       Tel:    +49-681-302-2133
DFKI GmbH &                          Fax:    +49-681-302-5076
Informatics, Saarland University   Email:    autexier at dfki.de
66123 Saarbruecken                   WWW: www.dfki.de/~serge/