William Mansky
Assistant Professor
Department of Computer Science
University of Illinois at Chicago
mansky1 at uic dot edu

1331 Science and Engineering Offices
851 S Morgan St, Chicago, IL 60607

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: I'm currently looking for PhD students! If you're interested in proving correctness of programs, formal logic, the behavior of programming languages, or anything else in the areas of programming language theory, logic, and concurrency, send me an email.


Last updated 4/22/19