Call for Participation - IJCAR'01 Verification Workshop (VERIFY'01)

[Serge Autexier <serge@dfki.de>]

**********************************************************************
***                First Call for Participation                    ***
**********************************************************************

			VERIFICATION WORKSHOP

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

		    in connection with IJCAR 2001

		     June 19, 2001, Siena, Italy

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

			CALL FOR PARTICIPATION

Traditionally, the verification of  system properties has been one  of
the main areas  of application for  automated theorem  proving. On the
one hand side, the formal development  of safety and security critical
systems  creates    numerous deduction problems   which   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 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  emphasis of  this
years workshop  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?

TOPICS

+ ATP techniques in verification      + Refinement & decomposition
+ Case studies (specification&verif.) + 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
+ Protocol verification               


IMPORTANT DATES

  Early registration:          *May 15, 2001*
  Verification workshop:        June 19, 2001
  IJCAR 2001:                June 20-23, 2001


PARTICIPATION

Participation   will be by invitation    only. All authors of accepted
papers  and  PC  members  have been   invited.  Other persons  who are
interested  in participating, will  be  requested to  send  a position
paper to verification-ws@ags.uni-sb.de  (Subject: `Position paper') by
May 13, 2001. Note that all participants must register to IJCAR.


LIST OF ACCEPTED REGULAR PAPERS 

  M. Breitling, J. Philipps (TU Munich, Germany):  
     Bridging System Views 

  Y. Chevalier, L. Vigneron (LORIA, France):  
     Towards Efficient Automated Verification of Security Protocols 

  D. Duffy (U. York, UK), J. Giesl (RWTH Aachen, Germany)       
     Induction for Specification Languages like Z* 

  N. Evans (Royal Holloway, UK)               
     A Practical Introduction to Using CSP and PVS to Prove 
     Authentication Properties of Security Protocols 

  A. Fioravanti (U. Rome, Italy), F. Massacci (U. Siena, Italy) 
     How to model (and simplify) the SET payment phase for automated 
     verification 

  R.P. Gore (ARP-ANU, Australia), P.T. Nguyen (CSE-ANU, Australia)      
     CardS4: Modal Theorem Proving on Java Smartcards 

  R. Hale (De Montford University, UK) 
     Using ITL for Codesign (Work in progress) 

  T. Ksiyatrakul, S. Older, S.-K. Chin (U. Syracuse, USA): 
     Formal Analysis of X.509 Certificates 


LIST OF ACCEPTED DISCUSSION PAPERS

  P. Fenkam (TU Vienna, Austria)         
     A Note On Proof-Carrying Code   
  
  A. Ireland  (Heriot-Watt, UK) 
     Formal Verification of High Integrity Software

For more information about the papers see the workshop webpage.


PROGRAM COMMITTEE

  S. Autexier (U. Saarbruecken, Co-Chair)
  D. Basin (U. Freiburg)
  R. Focardi (U. Venezia)
  R. Gorrieri (U. Bologna)
  A. Ireland (Heriot-Watt, Edinburgh)
  D. Kapur (U. New Mexico, Albuquerque)
  C. Kreitz (Cornell, Ithaca)
  H. Mantel (DFKI Saarbruecken, Co-Chair)
  F. Massacci (U. Siena)
  S. Schneider (Royal Holloway, London)


WORKSHOP WEB PAGE 
	 http://www.ags.uni-sb.de/verification-ws/index.html