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

I am now an assistant professor at the University of Illinois at Chicago. My new website is here.

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 Verified Software Toolchain 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 web server and database implementations, and to develop simple approaches to reasoning about fine-grained concurrency. I've written an introduction to verifying concurrent programs in VST, available here. 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.


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