VSL 2014: VIENNA SUMMER OF LOGIC 2014
VERIFY Home Page

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:

  1. 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).
  2. 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).