6th International Verification Workshop – VERIFY-2010

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

Edinburgh, July 20–21, 2010

in connection with IJCAR 2010

Keynote Speakers

V. Cortier (LORIA INRIA-Lorraine, France)
C. Jones (Newcastle University, UK)
A. Platzer (Carnegie Mellon University, USA)

Program & Workshop Chairs

M. Aderhold (TU Darmstadt)
S. Autexier (DFKI Bremen)
H. Mantel (TU Darmstadt)

Program Committee

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

Call for papers



Important dates

Abstract Submission Deadline: April 7, 2010
Paper Submission Deadline: April 11, 2010
Notification of acceptance: April 29, 2010
Final version due: May 17, 2010
Workshop date: July 20–21, 2010

Previous VERIFY workshops


If you need further information, do not hesitate to
contact the workshop chairs by sending an e-mail
to verify2010@mais.informatik.tu-darmstadt.de.


About the Workshop

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.

For automated theorem proving, each verification project is the source of numerous deduction problems that are not only interesting and challenging, but also of practical relevance. On the one hand, such proof obligations can serve as examples for experimenting with general-purpose deduction techniques and tools. On the other hand, deduction techniques can be tailored to typical classes of verification problems.

Tool support is essential in order to deal with the numerous proof obligations arising in practical verification. In particular, powerful theorem provers are required to provide a high degree of automation. Moreover, tool support is also necessary for making the development of large specifications feasible, for keeping ongoing developments in a consistent state, and for supporting the reuse of previously constructed specifications and proofs. Often, satisfactory tool support can only be achieved by combining different systems.

Engineering techniques are needed for making the formal modeling and analysis of complex information systems feasible. Specifications become more manageable when being developed in a modular fashion and on different levels of abstraction. When a well-defined engineering process is applied, verification techniques can be tailored to the deduction problems that typically originate from this process.

Applications include the verification of functional properties, of safety properties, of security properties, and of fault tolerance. Evaluation criteria like the Common Criteria, for instance, require the construction of formal security models that constitute a basis for a formal verification. Verification case studies are necessary for evaluating the feasibility of verification techniques in practice.

The VERIFY workshop series aims at bringing together people who are interested in the development of safety-critical 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 + Integration of ATPs and CASE-tools
+ Case studies (specification and verification) + Management of change
+ Combination of verification tools + Refinement and decomposition
+ Compositional and modular reasoning + Reliability of mobile computing
+ Experience reports on using formal methods + Reuse of specifications and proofs
+ Formal methods for fault tolerance + Safety-critical systems
+ Gaps between problems and techniques + Security models
+ Information-flow security + 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 paper: 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).

Submission of papers is via EasyChair at http://www.easychair.org/conferences/?conf=verify2010.

Final versions of accepted papers have to be prepared with LaTeX using the EasyChair class. Each accepted paper shall be presented at the workshop and at least one author of each paper must attend the workshop.


For each presentation there will be 40 minutes (including about 10 minutes discussion). For discussion papers, 15–20 minutes shall be reserved for discussion. The workshop program also includes several invited talks.

Workshop Proceedings

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

Markus Aderhold, Serge Autexier, Heiko Mantel
Last modified: July 26, 2010