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

Vienna, July 23–24, 2014

in connection with IJCAR 2014

VERIFY 2014 will by joint with ARW-DT

## Program & Workshop ChairsS. Autexier (DFKI Bremen, Germany)B. Beckert (Karlsruhe Institute of Technology, Germany) ## Program CommitteeW. Ahrendt (Chalmers University of Technology)J. (Middlesex University) I. Cervesato (Carnegie Mellon University) J. Fleuriot (University of Edinburgh) M. Huisman (University of Twente) D. Hutter (DFKI GmbH) R. Hähnle (Technical University of Darmstadt) D. Kapur (University of New Mexico) G. Klein (NICTA and UNSW) J. Leslie-Hurd (Intel Corporation) F. Martinelli (IIT-CNR) C. Meadows (NRL) S. Merz (Inria Nancy) T. Nipkow (TU München) L. Paulson (University of Cambridge) J. Schumann (SGT, Inc/NASA Ames) K. Stenzel (University of Augsburg) ## Call for papersPDF – ASCII## Important dates
## Previous VERIFY workshops## ContactIf you need further information, do not hesitate tocontact the workshop chairs by sending an e-mail to mailto:verify2014@informatik.uni-bremen.de?subject=Verify-2014. |
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 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 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 SystemsA non-exclusive list of application areas with these characteristics are
The scope of VERIFY includes topics such as
## SubmissionSubmissions 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=verify2014. 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. ## PresentationFor 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 invited talks. ## Workshop ProceedingsIn addition to informal proceedings, a special issue in a journal on the topic of the workshop is envisaged. Participants of VERIFY-2014 are particularly encouraged to submit a paper to the special issue, but other submissions will also be welcome. |

Serge Autexier, Bernhard Beckert Last modified: November 21, 2014