[Iris-Club] Fwd: [OWLS] OWLS returns tomorrow with Peter O'Hearn!

Derek Dreyer dreyer at mpi-sws.org
Wed Oct 13 15:32:35 CEST 2021


In case you hadn't seen this already, this talk (starting in 30
minutes) should be interesting.

The Zoom link is here:
https://us02web.zoom.us/j/177472153?pwd=MFgwd0EzY05QSGtpSDc2dU16aG9wdz09

Derek

---------- Forwarded message ---------
From: Alexandra Silva <alexandra.silva at gmail.com>
Date: Tue, Oct 12, 2021 at 3:10 PM
Subject: [OWLS] OWLS returns tomorrow with Peter O'Hearn!
To: <cl-owls at lists.cam.ac.uk>


Dear all,

It is a great pleasure to announce the first OWLS of this academic year,
which will take place tomorrow Wednesday 13th October at 2pm UTC!

Quentin Carbonneaux and Peter O'Hearn, from Facebook will talk about
Applying proof to a microkernel IPC mechanism

Please see below for an abstract! All details on how to join and
upcoming seminars can be found here:
https://www.cl.cam.ac.uk/events/owls/

Cheers,
Alexandra, Jamie, and Pawel



Facebook is building a new microkernel operating system as part of its AR/VR
strategy.  This talk describes a project to apply software verification to a
central part of the OS: the interpocess communication design.
We use Iris, an implementation of concurrent separation logic in the Coq
proof assistant, to verify two queue data structures used for IPC.
The verification effort uncovered algorithmic simplifications as well as
bugs in client code.  The simplifications involve the removal of redundant
operations in a performance-critical part of the kernel.
The proof work was completed in person months, not years, by engineers with
no prior familiarity with Iris. These findings are spurring further use of
verification at Facebook.
--------------------
Online Worldwide Seminar in Logic and Semantics (OWLS)
https://www.cs.bham.ac.uk/~vicaryjo/owls/



More information about the Iris-Club mailing list