Colloquium Details
Building Correct Programs
Speaker: William Mansky, Princeton University
Location: 60 Fifth Avenue 150
Date: February 9, 2018, 11 a.m.
Host: Thomas Wies
Synopsis:
Everyday code, written in imperative languages, is plagued by bugs: missed corner cases, logic errors, and even compiler bugs. Programming language theory and formal methods give us the techniques we need to prove that programs satisfy their specifications, are memory safe, and/or use concurrency and synchronization correctly. Several recent projects have demonstrated that we can construct bug-free software at scale, using logic, semantics, and interactive theorem proving. I will present my work in verifying two concurrent applications, a dynamic race detector and a messaging system for autonomous vehicles, and describe an ongoing project in verifying high-performance concurrent data structures. By combining detailed models of program behavior, state-of-the art logics for memory and concurrency, and tools for constructing and checking mathematical proofs, we can now formally guarantee that real-world programs are bug-free.
Speaker Bio:
William Mansky is an associate research scholar at Princeton University, working with Andrew Appel in the Verified Software Toolchain group. His research centers on formally modeling the behavior of programming languages, especially memory and concurrency behavior, and proving correctness of real-world programs. He received his PhD from the University of Illinois at Urbana-Champaign in 2014 under Elsa L. Gunter; his thesis described a framework for formal verification of compiler optimizations. He then spent two years as a postdoc at the University of Pennsylvania, working with Steve Zdancewic on formal semantics for the LLVM intermediate representation as part of the Vellvm project.
Notes:
In-person attendance only available to those with active NYU ID cards.