From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 89AC57F860 for ; Fri, 21 Feb 2014 16:45:59 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of serge.autexier@dfki.de) identity=pra; client-ip=134.96.191.185; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="serge.autexier@dfki.de"; x-sender="serge.autexier@dfki.de"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of serge.autexier@dfki.de) identity=mailfrom; client-ip=134.96.191.185; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="serge.autexier@dfki.de"; x-sender="serge.autexier@dfki.de"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@sea-mail.dfki.de) identity=helo; client-ip=134.96.191.185; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="serge.autexier@dfki.de"; x-sender="postmaster@sea-mail.dfki.de"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AiUCAAN0B1OGYL+5mWdsb2JhbABQCoNBUYMJp08BlWqBDhYOAQEBAQEICwsHFCiCSQZFBA01AgUaBwIRHTsSCwUCh2oIBao6oRYXgSmMX1yCNg8xNYEUBIhbj1iBM4URhiCHM4E/ X-IPAS-Result: AiUCAAN0B1OGYL+5mWdsb2JhbABQCoNBUYMJp08BlWqBDhYOAQEBAQEICwsHFCiCSQZFBA01AgUaBwIRHTsSCwUCh2oIBao6oRYXgSmMX1yCNg8xNYEUBIhbj1iBM4URhiCHM4E/ X-IronPort-AV: E=Sophos;i="4.97,519,1389740400"; d="scan'208";a="59629169" Received: from sea-mail.dfki.de ([134.96.191.185]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-CAMELLIA256-SHA; 21 Feb 2014 16:45:58 +0100 Received: from sea-mail.dfki.de (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id 9E84FC6FA5_30774B3B for ; Fri, 21 Feb 2014 15:45:55 +0000 (GMT) Received: from mail.dfki.de (lnv-104.sb.dfki.de [134.96.191.146]) (using TLSv1 with cipher DHE-RSA-AES256-SHA (256/256 bits)) (Client did not present a certificate) by sea-mail.dfki.de (Sophos Email Appliance) with ESMTPS id 6F090C6FA4_30774B3F for ; Fri, 21 Feb 2014 15:45:55 +0000 (GMT) Received: from mbp-autexier.informatik.uni-bremen.de (mbp-autexier.informatik.uni-bremen.de [134.102.218.176]) (using TLSv1 with cipher ADH-AES256-SHA (256/256 bits)) (No client certificate requested) by mail.dfki.de (Postfix) with ESMTPSA id 5AFCC3109B; Fri, 21 Feb 2014 16:45:57 +0100 (CET) Received: by mbp-autexier.informatik.uni-bremen.de (Postfix, from userid 501) id C542A1ECA5BD; Fri, 21 Feb 2014 16:45:57 +0100 (CET) To: caml-list@inria.fr Content-Type: text/plain; charset="UTF-8" Cc: serge.autexier@dfki.de Message-Id: <20140221154557.C542A1ECA5BD@mbp-autexier.informatik.uni-bremen.de> Date: Fri, 21 Feb 2014 16:45:57 +0100 (CET) From: serge.autexier@dfki.de (Serge Autexier) X-Validation-by: serge.autexier@dfki.de Subject: [Caml-list] First Call for Papers: 8th Verification Workshop (VERIFY 2014), Focus Theme: Verification Beyond IT Systems [Apologies for cross posting] FIRST 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: April 17th, 2014 Paper Submission Deadline: April 25th, 2014 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 Hähnle (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 München) Lawrence Paulson (University of Cambridge) Johann Schumann (SGT, Inc/NASA Ames) Kurt Stenzel (University of Augsburg)