[Caml-list] First Call for Papers: 8th Verification Workshop (VERIFY 2014), Focus Theme: Verification Beyond IT Systems

[Apologies for cross posting]

FIRST CALL FOR PAPERS

8th International Verification Workshop (VERIFY'14)
in connection with IJCAR 2014 at FLoC 2014
July 23–24, 2014, Vienna, Austria

http://vsl2014.at/verify


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 workshop series aims 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 2014 edition of VERIFY aims for extending the verification methods
for processes implemented in hard- and software to processes that may
well include computer-assistance, but have a large part or a frequent
interaction with non-computer-based process steps. Hence the 2014
edition will run under the focus theme

Verification Beyond IT Systems

A non-exclusive list of application areas with these characteristics
are

* Ambient assisted living
* Intelligent home systems and processes
* Business systems and processes
* Production logistics systems and processes
* Transportation logistics
* Clinical processes
* Social systems and processes (e.g., voting systems)

The scope of VERIFY includes topics such as

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

Submissions are encouraged in one of the following two categories:

A. Regular paper: Submissions in this category should describe
previously unpublished work (completed or in progress), including
descriptions of research, tools, and applications. Papers must be
5-14 pages long (in EasyChair style) or 6-15 pages long (in
Springer LNCS style).

B. Discussion papers: Submissions in this category are intended to
initiate discussions and hence should address controversial issues,
and may include provocative statements. Papers must be 3-14 pages
long (in EasyChair style) or 3-15 pages long (in Springer LNCS
style).

Important dates
Abstract Submission Deadline: April 17th, 2014
Paper Submission Deadline: April 25th, 2014
Notification of acceptance: May 20, 2014
Final version due: May 27, 2014
Workshop date: July 23–24, 2014

Submission is via EasyChair:
http://www.easychair.org/conferences/?conf=verify2014

Program Committee

Serge Autexier (DFKI) - chair
Bernhard Beckert (Karlsruhe Institute of Technology) - chair
Wolfgang Ahrendt (Chalmers University of Technology)
Juan Augusto (Middlesex University)
Iliano Cervesato (Carnegie Mellon University)
Jacques Fleuriot (University of Edinburgh)
Marieke Huisman (University of Twente)
Dieter Hutter (DFKI GmbH)
Reiner Hähnle (Technical University of Darmstadt)
Deepak Kapur (University of New Mexico)
Gerwin Klein (NICTA and UNSW)
Joe Leslie-Hurd (Intel Corporation)
Fabio Martinelli (IIT-CNR)
Catherine Meadows (NRL)
Stephan Merz (INRIA Lorraine)
Tobias Nipkow (TU München)
Lawrence Paulson (University of Cambridge)
Johann Schumann (SGT, Inc/NASA Ames)
Kurt Stenzel (University of Augsburg)


--
Caml-list mailing list. Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs