William Mansky
Assistant Professor
Department of Computer Science
Contact
Building & Room:
1331 SEO
Address:
851 S. Morgan St, MC 152, Chicago, IL, 60607
Office Phone:
Email:
Related Sites:
About
Research Interests:
I'm interested in the semantics, analysis, and correctness of programs, especially concurrent programs. I've done work 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 working on building tools and techniques for proving the correctness of concurrent C programs, using the Verified Software Toolchain(code here). I 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.
More generally, I'm interested in bridging the gap between programming and program verification, providing better tools for programmers to understand the effects of code as they write it, and making it easier to verify code as it's written. I'd like to make it possible for every C programmer to write proved-correct code.
Current Projects:
- The DeepSpec Web Server, with the DeepSpec team
- Proving correctness of concurrent programs with C11 atomic operations
- Verifying single-node database implementations, with Lennart Beringer
I'm currently looking for PhD students! If you're interested in formal logic, programming language behavior, and/or software correctness, send me an email.
Selected Publications
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server, Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honore, William Mansky, Benjamin C. Pierce, Steve Zdancewic. CPP 2019.
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
Education
Ph.D., Computer Science, University of Illinois, Urbana-Champaign