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 730347EE80 for ; Wed, 20 Mar 2013 05:57:34 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of owre@csl.sri.com) identity=pra; client-ip=128.18.84.133; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="owre@csl.sri.com"; x-sender="owre@csl.sri.com"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of owre@csl.sri.com) identity=mailfrom; client-ip=128.18.84.133; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="owre@csl.sri.com"; x-sender="owre@csl.sri.com"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@brightmail-internal4.sri.com) identity=helo; client-ip=128.18.84.133; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="owre@csl.sri.com"; x-sender="postmaster@brightmail-internal4.sri.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AtwDAJRASVGAElSFmWdsb2JhbABDDogBvkUWDgEBAQEBCAsLBxQKHjkBAYFrBgEBGgZDAg05AgUhAgIPT4gmDK8ugkCQFhWBDpAggRMDiHWPCopMh2Jf X-IPAS-Result: AtwDAJRASVGAElSFmWdsb2JhbABDDogBvkUWDgEBAQEBCAsLBxQKHjkBAYFrBgEBGgZDAg05AgUhAgIPT4gmDK8ugkCQFhWBDpAggRMDiHWPCopMh2Jf X-IronPort-AV: E=Sophos;i="4.84,876,1355094000"; d="scan'208";a="8411556" Received: from brightmail-internal4.sri.com ([128.18.84.133]) by mail2-smtp-roc.national.inria.fr with ESMTP; 20 Mar 2013 05:57:32 +0100 X-AuditID: 80125485-b7fc16d00000612f-5a-514941ba50e0 Received: from mx0.csl.sri.com (mx0.csl.sri.com [130.107.1.30]) (using TLS with cipher AES256-SHA (AES256-SHA/256 bits)) (Client did not present a certificate) by brightmail-internal4.sri.com (SRI Internal SMTP Gateway) with SMTP id 70.D3.24879.AB149415; Tue, 19 Mar 2013 21:57:30 -0700 (PDT) Received: from ubi (ubi.csl.sri.com [130.107.15.8]) by mx0.csl.sri.com (8.14.3/8.14.2) with ESMTP id r2K4vN3l038491 (version=TLSv1/SSLv3 cipher=AES256-SHA bits=256 verify=NO); Tue, 19 Mar 2013 21:57:23 -0700 (PDT) (envelope-from owre@csl.sri.com) Received: from owre (helo=ubi) by ubi with local-esmtp (Exim 4.72) (envelope-from ) id 1UIB5X-00052u-EQ; Tue, 19 Mar 2013 21:57:23 -0700 To: acl2@utlists.utexas.edu, afsec@afsec.asr.cnrs.fr, amast@cs.utwente.nl, calculemus-ig@mathweb.org, caml-list@inria.fr, comlab@comlab.ox.ac.uk, concurrency@listserver.tue.nl, coq-club@pauillac.inria.fr, event@in.tu-clausthal.de, fmcad@utlists.utexas.edu, gdr-im@gdr-im.fr, hol-info@lists.sourceforge.net, isabelle-users@cl.cam.ac.uk, lics@research.bell-labs.com, lprolog@cs.umn.edu, matita@cs.unibo.it, mizar-forum@mizar.uwb.edu.pl, poplmark@lists.seas.upenn.edu, prog-lang@diku.dk, pvs@csl.sri.com, qpq-general@qpq.org, sal@csl.sri.com, strqds@laas.fr, theorem-provers@ai.mit.edu, theory-logic@cs.cmu.edu, theorynt@listserv.nodak.edu, types-announce@lists.seas.upenn.edu, verimag-news@imag.fr, yices@csl.sri.com X-Mailer: MH-E 8.2; nmh 1.3; GNU Emacs 23.1.1 MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Date: Tue, 19 Mar 2013 21:57:23 -0700 Message-ID: <19399.1363755443@ubi> From: Sam Owre X-Brightmail-Tracker: H4sIAAAAAAAAA02RW0iTYRjHe/d92z5Hy68p+qKVNKnQ0JKEXqk83OSbBGl4kd3Yyi8dbmqb iQbRUgyZkJYHmlbOOXQeyrC0tYna0KmLbA6TGZkkWR4SdM40dZKHBO9+z/N/nt/NnyIEI6QP JU7LZGRpIomQwyNzU8GhIEPUhbiTqjIh6tHXA/S0qY+N7J/SkKL1PUAO/SsSzbV0sNGKdYCN fql0BGp02lnI7vpOoCLLAhdND1aS6FHNfYAKTRgtzpZzkbP3PNJNrBBooe4zGxWuHkSvZ3Vc tFhbxUaGr7VcZFzrZ6Gi+WkWMpWQaPB3OyfSBy8rh0hc0JeJW/N7STxSHI7V3RexRaHm4NLR XAIvzzSzcVPxEsDrJRoSm835BFaWeODHkyYSq5b1ABvMnVxsVC+wYuFV3tkkRiLOYmQnwq/x UsyjWlZG1dHsorcFhAK4/JSAoiAdCu3mMCVw20AvaP3WzFECHiWgG1jwjXmVuz2sA/igq/N/ 8gTAAoeNvfniSb/gQI0xcZM96EDYo7QS26ogOK9RcTeZT++H/aof5CYT9DG49txGbPNxWFs9 s8UkfQROabqJ7XshrLIpt/wc+jDM+1JNFIN9FbtUFbtUFbtUakA0gAPXZeLklEypSCwJ2qk5 NFguEwffSJe2gI3CFYL4fD3QtYeYAE0B4V7+VCWOE7BFWfIcqQlAihB68p3DGyt+kijnDiNL T5TdljByE/ClSKE3/89p90sCOlmUyaQyTAYj20lZlJuPAiQMhgcguDjQJoyyJyRzempiQn9i +9hchc7XP8IdlYY4zSzpzL3Y6L8tkvhJyy2V9mHb+N+XYQJRcePQGe3luokO45i3K9vqZdij r6wvqqnjfxzBZQlNp6ZdERZbniPA4R8cU30ueviDYelmZNv4s64hv7LKK5berHLtXec7ISlP EYUEEjK56B8cXvCL7AIAAA== Subject: [Caml-list] VeriSure Workshop Call for Papers ********************************************************** CALL FOR PAPERS ********************************************************** VeriSure: Verification and Assurance In association with Computer-Aided Verification (CAV) 2013 July 14, 2013, Saint Petersburg, Russia http://fm.csl.sri.com/VeriSure/ Workshop Organizers Sam Owre, Natarajan Shankar, and John Rushby, SRI International *** Workshop Description *** The purpose of this workshop is to explore issues at the conjunction of computer-aided verification and system assurance. An autonomous car, for example, must safely negotiate an environment that is imperfectly and incompletely modeled, while using actuators that are themselves imperfect, and guided by fallible sensors whose data requires delicate interpretation and fusion. Assurance here clearly requires more than verification, but can build on verified foundations. In general, computer-aided verification is usually performed in support of a larger activity whose goal is to provide assurance for a decision with large consequences. The decision may be to send a hardware design for fabrication or to release a commercial software product, in which cases the consequences are economic, or it may be to deploy a system in a context with potential consequences for societal safety or security. In all these cases, verification will be just one of many strands of evidence that contribute to system assurance, and the overall structure of the assurance may be specified or constrained by regulation or certification requirements. This workshop will explore challenges and opportunities posed for computer-aided verification by the larger context of system assurance. One immediate set of challenges arises from the (recursive) need to provide assurance for the claims delivered by computer-aided verification itself. Related is the challenge of providing assurance for the assumptions and requirements with respect to which the verification is performed. These challenges are situated in pragmatic engineering settings where choices must be made about what should be verified, and to what level of detail, and what should or must be assured by other means (such as testing, human review, or runtime monitoring), and how all these should be combined. Opportunities arise from the possibility of formalizing and verifying aspects of the larger assurance activity, stimulated by recent proposals that this should be structured as an assurance "case." An assurance case is composed of claims, argument, and evidence, where the argument justifies claims (e.g., for security or safety) based on evidence about the system and its development. An interesting complication is that many top-level claims are probabilistic (e.g., 10-9 for certain aircraft software) while traditional formal verification is unconditional. We solicit papers on relevant topics, which include but are not restricted to the following. We encourage exploratory work that will stimulate discussion. o Quantitative and qualitative assurance claims and arguments o Integration of formal verification with assurance and with assurance cases o Modular and incremental methods of verification and assurance o Toolchains for integrated assurance arguments o Soundness guarantees for tools, toolchains, and workflows o Certification and regulatory requirements and standards o Experience reports and challenges The program will include invited speakers, presentation of selected papers, and discussion. The workshop is colocated with CAV 2013 in Saint Petersburg, Russia *** Invited Speakers *** Robin Bloomfield, City University and Adelard Others to be announced *** Workshop Committee *** Jean-Christophe Filli=C3=A2tre, LRI Universit=C3=A9 Paris Sud, France Mike Gordon, Cambridge University, UK Sofia Guerra, Adelard, UK Michael Holloway, NASA Langley, USA Michaela Huhn, TU-Clausthal, Germany Florent Kirchner, CEA, France Gerwin Klein, NICTA, Australia Tom Maibaum, McMaster University, Canada Bertrand Meyer, ETH Zurich, Switzerland Grigori Mints, Stanford University, USA Harald Ruess, FORTISS, Germany Oleg Sokolsky, University of Pennsylvania, USA Virginie Wiels, ONERA, France *** Important Dates *** Position papers due Soon Reviews/decisions TBA Camera ready versions due TBA VeriSure Workshop July 14 Note: We ask potential participants to apply for a visa invitation letter as soon as possible (even if their trip plans may change later). For further details please check the CAV Visa page at http://cav2013.forsyte.at/visa/ *** Electronic Submissions *** Submissions should be in PDF format between 3-12 pages. We recommend the guidelines for ACM SIG Proceedings. The submissions page is open at https://www.easychair.org/conferences/?conf=3Dverisure2013