[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS] Verify 2010 - 1st Call for Papers



              [Apologies for possible multiple postings]


                          CALL FOR PAPERS

        6th International Verification Workshop (VERIFY-2010)

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

          in connection with IJCAR-2010 at FLoC-2010

               July 20-21, 2010, Edinburgh, UK

	 [http://www.mais.informatik.tu-darmstadt.de/verify2010/]

*********************  Keynote speakers ******************************
**          Véronique Cortier (LORIA INRIA-Lorraine, France)        **
**         Cliff Jones (Newcastle University, UK)                   **
**         André Platzer (Carnegie Mellon University, USA)          **
**********************************************************************

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?

The scope of VERIFY includes topics such as

+ ATP techniques in verification      + Information flow security
+ Case studies                        + Integration of ATPs and CASE-tools
  (specification and verification)    + Management of change
+ Combination of verification systems + Refinement and decomposition
+ Compositional and modular reasoning + Reliability of mobile computing
+ Experience reports on using         + Reuse of specifications and proofs
  formal methods                      + Safety-critical systems
+ Formal methods for fault tolerance  + Security models
+ Gaps between problems and           + Tool support for formal methods
  techniques


Submissions are encouraged in one of the following two categories:

 A.  Regular papers:  Submissions  in  this category  should  describe
     previously unpublished work (completed or in progress), including
     descriptions of research,  tools, and  applications.  Papers must
     be  6-15  pages  long,  formatted  following  the  Springer  LNCS
     guidelines.

 B.  Discussion papers: Submissions  in this category are  intended to
     initiate discussions and should address controversial issues, and
     may include provocative   statements.   Papers must be 3-15 pages
     long, formatted following the Springer LNCS guidelines.

Submission of papers is via EasyChair:
        http://www.easychair.org/conferences/?conf=verify2010
Upon submission, the category (either A or B) should be indicated.

Each  accepted paper shall be presented  at the workshop  and at least
one author of each paper must attend the workshop.

In addition to informal proceedings,  we envisage a special issue in a
journal on the topic of the workshop.  Participants of VERIFY-2010 are
particularly encouraged  to submit a paper  to the special issue,  but
other submissions will also be welcome.

Program & Workshop Co-Chairs
  M. Aderhold   (TU Darmstadt)
  S. Autexier   (DFKI Bremen)
  H. Mantel     (TU Darmstadt)

Program Committee
  B. Beckert    (Karlsruhe Institute of Technology)
  I. Cervesato  (Carnegie Mellon University)
  C. Fournet    (Microsoft Research)
  J. Guttman    (Worcester Polytechnic Institute)
  R. Hähnle     (Chalmers University)
  J. Hurd       (Galois Inc.)
  D. Hutter     (DFKI Bremen)
  P. Jackson    (University of Edinburgh)
  C. Jones      (Newcastle University)
  D. Kapur      (University of New Mexico)
  J.-P. Katoen  (RWTH Aachen)
  G. Klein      (NICTA)
  G. Lowe       (University of Oxford)
  F. Martinelli (CNR Pisa)
  C. Meadows    (Naval Research Laboratory)
  D. Pichardie  (INRIA Rennes)
  G. Schneider  (University of Gothenburg)
  J. Schumann   (NASA Ames Research Center)
  C. Walther    (TU Darmstadt)

Important dates:
  Submission deadline:         March 22, 2010
  Notification of acceptance:  April 29, 2010
  Final version due:           May 17, 2010
  Workshop date:               July 20-21, 2010

Workshop e-mail: verify2010@mais.informatik.tu-darmstadt.de