William Mansky
Postdoctoral Researcher
Department of Computer and Information Science
University of Pennsylvania
wmansky at seas dot upenn dot edu

I will be starting a postdoc at Princeton in September.
Curriculum Vitae

Research Interests

My main research topics are compiler verification, programming language semantics (especially for intermediate languages), and formalizing memory models (both sequential and concurrent).

I am currently working with Professor Steve Zdancewic on the Vellvm project. As part of our redesign of Vellvm, I am investigating abstract interfaces for sequential memory models; a Coq formalization of a preliminary version can be found here. I am also developing reasoning principles that apply across concurrent memory models, and working to verify dynamic race detection algorithms.

I did my grad work at UIUC under Elsa Gunter. I developed VeriF-OPT, a framework for specifying and verifying compiler optimizations.


SlimFast: Reducing Metadata Redundancy in Sound and Complete Dynamic Data Race Detection, Yuanfeng Peng, Christian DeLozier, Ariel Eizenberg, William Mansky, Joseph Devietti. To be submitted to ASPLOS 2017.

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, Victor 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 2/1/16