VERIFY will be joint with the ARW-DT workshop.
Overview
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
Detailed information on VERIFY 2014 can be found on the VERIFY 2014 website.
Organization & Program Committee
Important Dates
| Abstract submission deadline: | May 5th, 2014 (extended) |
| Submission deadline: | May 5th, 2014 (extended) |
| Workshop date | July 23–24, 2014 |
Submission (via EasyChair)
Submissions are encouraged in one of the following two categories:
- 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).
- 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).