William Mansky
Associate Research Scholar
Department of Computer Science
Princeton University
wmansky at cs dot princeton dot edu

I am currently searching for tenure-track academic positions.
Curriculum Vitae
Research Statement
Teaching Statement

Research Interests

I'm interested in the semantics, analysis, and correctness of programs, especially concurrent programs. I've worked in compiler and program verification, programming language semantics for low-level languages, and formalizing memory models (both sequential and concurrent). My main tools are the interactive theorem provers Coq and Isabelle.

I am currently working with Andrew Appel on the VST project (code here), building tools and techniques for proving the correctness of concurrent C programs. We aim to prove correctness of realistic concurrent systems code, including distributed communication and file systems, and to develop simple approaches to reasoning about fine-grained concurrency. I previously worked with Steve Zdancewic on the Vellvm project, a formal semantics and optimization verification framework for LLVM.

I did my grad work at UIUC under Elsa Gunter. I developed VeriF-OPT, a framework for specifying and verifying compiler optimizations. The core of the framework is a domain-specific language for specifying and executing program transformations, now called Morpheus.


Proving Atomicity of Release-Acquire Concurrent Programs, William Mansky, Andrew W. Appel. In progress.

A Verified Messaging System, William Mansky, Andrew W. Appel, Aleksey Nogin. OOPSLA 2017.

BARRACUDA: Binary-level Analysis of Runtime RAces in CUDA Programs, Ariel Eizenberg, Yuanfeng Peng, Toma Pigli, William Mansky, Joseph Devietti. PLDI 2017.

Verifying Dynamic Race Detection, William Mansky, Yuanfeng Peng, Steve Zdancewic, Joseph Devietti. CPP 2017.

Specifying and Executing Optimizations for Generalized Control Flow Graphs, William Mansky, Elsa L. Gunter, Dennis Griffith, Michael D. Adams. Science of Computer Programming vol. 130, 2016.

An Axiomatic Specification for Sequential Memory Models, William Mansky, Dmitri Garbuzov, Steve Zdancewic. CAV 2015.

A Formal C Memory Model Supporting Integer-Pointer Casts, Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, Viktor Vafeiadis. PLDI 2015.

Symbolic Analysis Tools for CSP, Liyi Li, Elsa L. Gunter, William Mansky. ICTAC 2014: 295-313

A Cross-Language Framework for Verifying Compiler Optimizations, William Mansky, Elsa L. Gunter. Presented at LOLA 2014.

Verifying Optimizations for Concurrent Programs, William Mansky, Elsa L. Gunter. WPTE@RTA/TLCA 2014: 15-26

Specifying and Verifying Program Transformations with PTRANS, William Mansky. PhD thesis.

Specifying and Executing Optimizations for Parallel Programs, William Mansky, Dennis Griffith, Elsa L. Gunter. GRAPHITE 2014: 58-70

The PTRANS Specification Language, William Mansky. UIUC Technical Report, 2014.

Using Locales to Define a Rely-Guarantee Temporal Logic, William Mansky, Elsa L. Gunter. ITP 2012: 299-314

Toward a multi-method approach to formalizing human-automation interaction and human-human communications, Ellen J. Bass, Matthew L. Bolton, Karen M. Feigh, Dennis Griffith, Elsa L. Gunter, William Mansky, John M. Rushby. SMC 2011: 1817-1824

A Framework for Formal Verification of Compiler Optimizations, William Mansky, Elsa L. Gunter. ITP 2010: 371-386

Last updated 10/10/17