[Apologies for cross posting, Deadline extended to *May 5th, 2014*]
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: May 5th, 2014 (extended)
Paper Submission Deadline: May 5th, 2014 (extended)
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 Haehnle (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 Munich)
Lawrence Paulson (University of Cambridge)
Johann Schumann (SGT, Inc/NASA Ames)
Kurt Stenzel (University of Augsburg)
--
Karlsruhe Institute of Technology (KIT)
Institute for Theoretical Informatics
Application-oriented Formal Verification
Prof. Dr. Bernhard Beckert
Am Fasanengarten 5, Building 50.34, Room 224
D-76131 Karlsruhe, GERMANY
Phone: +49 721 608-44025
Fax: +49 721 608-43088
E-mail: [log in to unmask]
http://formal.iti.kit.edu
KIT -- University of the State of Baden-Wuerttemberg and
National Laboratory of the Helmholtz Association
|
