CFP: CADE Verification Workshop (VERIFY'02)

[Serge Autexier <serge@dfki.de>]

[Apologies for multiple copies of this announcement]

		   VERIFICATION WORKSHOP - VERIFY'02

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

 	         in connection with CADE at FLoC 2002

		 July 25-26, 2002, Copenhagen, Denmark

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


			    CALL FOR PAPERS

Traditionally, verification   has  been one   of    the main  areas   of
application for  automated theorem proving.  On  the one  hand side, the
formal development of  safety    or security critical  systems   creates
numerous  deduction   problems   that  are not    only   interesting and
challenging   but  also  of practical  relevance.  On    the other hand,
automated  theorem  proving offers the means   to reduce the development
burden in such formal developments, thus making them feasible.

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

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

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
chip-cards 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 modeling of security requirements
and  the  development of  powerful theorem  proving support.  Therefore,
submissions in this area are especially encouraged.

TOPICS include (but are not limited to)

 + Access control                              + Protocol verification 
 + ATP techniques in verification              + Refinement &
decomposition
 + Case studies (specification & verification) + Reuse of specifications
& proofs
 + Combination of verification systems         + Safety critical systems
 + Compositional & modular reasoning           + Security for mobile
computing
 + Fault tolerance                             + Security models
 + Gaps between problems & techniques          + Verification systems
 + Information flow control                

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.


SUBMISSIONS are encouraged in one of the following two categories:

A. Regular paper: Submissions in this category should describe completed
   work or work  in progress, including descriptions of research, tools, 
   and applications.  Papers should be in  postscript format, at most 10 
   pages (10- or 11-point font and reasonable margins on A4 paper).

B. Panel proposals:  Submissions  in  this   category  are  intended  to 
   initiate discussions and should address topics  that are in the
focus  
   of the workshop.  Proposals  for  panel sessions should  not exceed 5 
   pages,  contain  a list of possible panelists, and  an  indication
of  
   which of those panelists have confirmed participation.


SUBMISSION DETAILS 

Please    submit papers    in     postscript  format   by    e-mail   to
verification-ws@ags.uni-sb.de   (Subject:  `Paper  submission').    Upon
submission, the  category (either A or  B) must  be indicated, and name,
address, and e-mail of  the  contact author should  be included  in  the
e-mail.

Authors of  regular papers who  think  that their  submission is  in the
interest   of FCS   as   well  as VERIFY   may  indicate   this in their
submission.  Such papers can  be submitted to  either FCS or VERIFY, but
will be considered jointly by the program committees of both workshops.


WORKSHOP PROCEEDINGS 

The workshop   proceedings will  be distributed   at the workshop  as  a
collection of the accepted papers and  will also be  published as a DIKU
technical report.  Final versions of accepted papers have to be prepared
with LaTeX. LaTeX style guidelines for final versions will be announced.

The  publication of  selected papers from  FCS  and VERIFY in  a special
issue  of  a journal is considered  (possibly  in cooperation with other
workshops), but has not yet been decided upon.


PROGRAM COMMITTEE

 S. Autexier (U. Saarbrücken, Co-Chair)
 D. Basin (U. Freiburg)
 I. Cervesato (ITT Industries)
 R. Focardi (U. Venezia)
 R. Hähnle (Chalmers U.)
 N. Heintze (Agere Systems)
 A. Ireland (Heriot-Watt, Edinburgh)
 D. Kapur (U. New Mexico, Albuquerque)
 C. Kreitz (Cornell, Ithaca)
 H. Mantel (DFKI Saarbrücken)
 F. Martinelli (CNR Pisa)
 F. Massacci (U. di Trento)
 C. Meadows (NRL)
 S. Schneider (Royal Holloway, U. London) 


IMPORTANT DATES

Submission deadline:         April 22, 2002
Notification of acceptance:    May 31, 2002
Final version due:          to be announced
Early registration:         to be announced
Verification workshop:     July 25-26, 2002
FLoc 2002:         July 20 - August 1, 2002


WORKSHOP WEB PAGE 

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