VeriSure Workshop Call for Papers

[Sam Owre]

**********************************************************
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âtre, LRI Université 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=verisure2013