VeriSure: Verification and Assurance

23 July 2014, Vienna, Austria

In association with Computer-Aided Verification (CAV) 2014, part of the Vienna Summer of Logic

 *NEW* The VeriSure Program is now available from the VSL Website.
Note that early registration ends on 8 June.

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. Furthermore, verification generally employs conventional logic, whereas argumentation is often framed within some form of defeasible reasoning.

We solicit position papers, experience reports, and research papers on relevant topics, which include but are not restricted to the following.

Submissions do not need to be full papers: this is workshop and we are looking for interesting experience, work, and ideas (possibly preliminary and exploratory) that will stimulate discussion and thought.

This will be the second VeriSure Workshop: the first was held at CAV 2013 in St. Petersburg, Russia, and the program is available here.

Workshop Committee

Important Dates

Position papers due26 May 2014
Reviews/decisions6 June 2014
Camera ready versions due10 June 2014
VeriSure Workshop23 July 2014

Electronic Submissions

Submissions should be in PDF format between 3-12 pages. We recommend the guidelines for ACM SIG Proceedings. The submissions page at Easychair is open.

Workshop Location

The workshop is colocated with CAV 2014 in Vienna, Austria

Workshop Organizers

John Rushby, SRI International