Verification Workshop - VERIFY'02

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

Copenhagen, Denmark, July 25-26, 2002

in connection with FLOC 2002


Program & Workshop Co-Chairs

S. Autexier (U. Saarbrücken)
H. Mantel (DFKI Saarbrücken)

Program Committee

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)
F. Martinelli (CNR Pisa)
F. Massacci (U. di Trento)
C. Meadows (NRL)
S. Schneider (Royal Holloway, U. London)

Call for papers

Postscript, pdf, ASCII

FLOC 2002

Important dates

Submission Deadline: April 22, 2002
Notification of acceptance: May 31, 2002
Final version due: June 25, 2002
Early registration: June 15, 2002
Workshop date: July 25-26, 2002

Contact

If you need further information do not hesitate
to contact us by sending an e-mail to verification-ws@ags.uni-sb.de (Subject: `Information').

Topic

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 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)

+ Access control + Protocol verification
+ ATP techniques in verification + Refinement and decomposition
+ Case studies (specification and verification) + Reuse of specifications and proofs
+ Combination of verification systems + Safety critical systems
+ Compositional and modular reasoning + Security for mobile computing
+ Fault tolerance + Security models
+ Gaps between problems and 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.

Submission

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 proposal: 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.

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.


Serge Autexier
Last modified: Fri Jun 14 14:14:36 MEST 2002 Created: Mon Dec 11 10:17:33 MET 2000