William Mansky
Assistant Professor
Department of Computer Science
Contact
- Building & Room:
- CDRLC 4450
- Address:
- 850 W. Taylor St, MC 152, Chicago, IL 60607
Email:
Related Sites:
About
Research Interests:
My research interests include 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 tool is the Rocq interactive theorem prover.
I am working on building tools and techniques for proving the correctness of concurrent C programs, using the Verified Software Toolchain (VST) and Iris. I aim to prove correctness of realistic concurrent systems code, including web server and database implementations, and to develop simpler approaches to reasoning about fine-grained concurrency. I am the main designer of VST 3.0, which rebuilds VST on top of Iris’s simple and general foundations, so we can apply the cutting-edge verification techniques of Iris to actually-running C code.
I’m also 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. This means thinking about the user experience of verification, not just writing proofs ourselves. If this sounds interesting to you, let me know!
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