Write a Blog >>
SPLASH 2017
Sun 22 - Fri 27 October 2017 Vancouver, Canada
Thu 26 Oct 2017 16:15 - 16:37 at Regency C - Verification in Practice Chair(s): Davide Ancona

We present a concurrent-read exclusive-write buffer system with strong correctness and security properties. Our motivating application for this system is the distribution of sensor values in a multicomponent vehicle-control system, where some components are unverified and possibly malicious, and other components are vehicle-control-critical and must be verified. Valid participants are guaranteed correct communication (i.e., the writer is always able to write to an unused buffer, and readers always read the most recently published value), while invalid readers or writers cannot compromise the correctness or liveness of valid participants. There is only one writer, all operations are wait-free, and there is no extra process or thread mediating communication. We prove the correctness of the system with valid participants by formally verifying a C implementation of the system in Coq, using the Verified Software Toolchain extended with an atomic exchange operation. The result is the first C-level mechanized verification of a nonblocking communication protocol.

Thu 26 Oct

Displayed time zone: Tijuana, Baja California change

15:30 - 17:00
Verification in PracticeOOPSLA at Regency C
Chair(s): Davide Ancona University of Genova
15:30
22m
Talk
A Model for Reasoning about JavaScript Promises
OOPSLA
Magnus Madsen University of Waterloo, Ondřej Lhoták University of Waterloo, Canada, Frank Tip Northeastern University
DOI
15:52
22m
Talk
Robust and Compositional Verification of Object Capability Patterns
OOPSLA
David Swasey MPI-SWS, Germany, Deepak Garg Max Planck Institute for Software Systems, Derek Dreyer MPI-SWS
DOI
16:15
22m
Talk
A Verified Messaging System
OOPSLA
William Mansky Princeton University, Andrew W. Appel Princeton, Aleksey Nogin HRL Laboratories, LLC
DOI
16:37
22m
Talk
Who Guards the Guards? Formal Validation of the ARM v8-M Architecture Specification
OOPSLA
DOI