Colloquium Details
Verifying Concurrent, Crash-Safe Systems
Speaker: Joseph Tassarotti, Boston College
Location: 60 Fifth Avenue 150
Date: April 1, 2022, 11 a.m.
Host: Jinyang Li
Synopsis:
In recent years, formally verified proofs of correctness have been
developed for several realistic software systems. Despite these
successes, certain aspects of programs remain difficult to verify. One
approach to address this challenge is to develop new program logics that
provide specialized reasoning principles. In this talk, I will present
Perennial, a program logic for proving that concurrent systems are
crash-safe, meaning that they can recover from failures caused by
interruptions such as power loss. Crash-safety is difficult to reason
about because the combination of concurrent interleavings and the
possibility of interruption from crashes at any point introduces a wide
range of non-determinism. Perennial's features allow a proof developer
to avoid explicitly reasoning about this non-determinism, making it
possible to scale verification to larger systems. In particular, I will
describe how Perennial has been used in the verification of DaisyNFS, a
Network File System server.
Speaker Bio:
Joseph Tassarotti is an Assistant Professor in the Computer Science
Department at Boston College. He received his Ph.D. from Carnegie Mellon
University, where he was advised by Robert Harper and was supported by
an NDSEG fellowship. He was then a postdoctoral associate at MIT in the
PDOS group. His research interests are in formal verification and
programming languages, with a focus on applications to randomized and
concurrent programs.
Notes:
In-person attendance only available to those with active NYU ID cards.