The Coq mailing list

["Mayo, Jackson" <jmayo AT sandia.gov>]

CALL FOR ABSTRACTS

Workshop on High-Consequence Control Verification

http://www.sandia.gov/hccv/

July 18, 2016 - Toronto, Ontario, Canada

In conjunction with the 28th International Conference on Computer Aided
Verification (venue and registration information will be available at
http://i-cav.org/2016/).

Abstract submissions describing practical applications of high-consequence
control verification are especially encouraged.


DATES

Abstract submission (1 page maximum): May 18, 2016
Notification: May 25, 2016
Workshop: July 18, 2016


PRELIMINARY PROGRAM

Confirmed invited speaker:
Sanjit Seshia (University of California, Berkeley)

Additional contributors:
Karla Morris (Sandia/California) and Colin Snook (University of Southampton)
Philip Johnson-Freyd (University of Oregon)
Aadithya Karthik (Sandia/New Mexico)
Lee Pike (Galois, Inc.)
Toby Wilkinson and Michael Butler (University of Southampton)


SCOPE

The Workshop on High-Consequence Control Verification (HCCV) focuses on formal
methods concepts and techniques to ensure the highest levels of reliability,
safety, and security for digitally controlled devices, including the effects
of possibly extreme physical environments. The workshop targets applications
where the severe consequences of failure justify extraordinary investments not
appropriate for less critical devices -- including special methodologies at
the design stage to enable verifying stringent reliability, safety, and
security requirements in the resulting devices under both nominal and
out-of-nominal (fault) conditions. Such needs exist in domains including
defense, medical devices, and scientific instrumentation.

The willingness to make greater investments for small but high-consequence
devices can provide an opportunity to leverage emerging, more powerful formal
methods techniques that may currently be considered too costly for
"mainstream" industrial applications. Novel ideas for design and analysis
techniques that promote in-depth verifiability are of strong interest for
these high-consequence digital controllers. The HCCV workshop offers a new
forum for engagement among formal methods researchers, tool developers, and
practitioners.

Topics of interest include:

  * Theory and techniques for formally verified high-consequence digital
    design (via model checking and/or theorem proving), such as:
      - Abstraction/refinement
      - Correct-by-construction synthesis
      - Exhaustive or probabilistic analysis of fault consequences
      - Incorporation of analog physics

  * Applications to safety-critical digitally controlled devices in domains
    such as:
      - Defense
      - Medical
      - Supervisory control and data acquisition (SCADA)

Important notes:

  * Submissions should target requirements for high-consequence devices, *not*
    general-purpose software verification or cybersecurity.

  * Submissions should target mathematical analyzability of designs, *not
    merely* testing- and simulation-based verification or the use of standard
    electronic design automation (EDA) tools.


SUBMISSION

Abstracts of up to 1 page in PDF format should be submitted at
https://easychair.org/conferences/?conf=hccv2016 on or before May 18, 2016.
Each accepted abstract will be allotted a speaking slot. The collection of
accepted abstracts will be made available for download from the workshop
website.


ORGANIZERS

Jackson R. Mayo (co-chair)
Sandia National Laboratories
Livermore, California, United States
jmayo AT sandia.gov

Michael J. Butler (co-chair)
University of Southampton, United Kingdom
mjb AT ecs.soton.ac.uk