Date & Time:
February 2, 2024 12:00 pm – 1:30 pm
02/02/2024 12:00 PM 02/02/2024 01:30 PM America/Chicago William Mansky (UIC)- Foundational C Verification with VST and Iris

Abstract: The strongest way to guarantee a program’s correctness is to verify it with a program logic implemented in an interactive theorem prover. Two systems for this kind of verification are the Verified Software Toolchain (VST), which connects to the CompCert verified C compiler to provide guarantees down to assembly, and Iris, a language-independent separation logic framework that has been the focus of a huge amount of recent research across many application domains and language features. In this talk, I aim to give a taste of the theory and practice of these foundational program verification tools. I will review the basic principles of separation logic, describe how Iris implements them via a flexible notion of “resource algebra” and an elegant proof mode, and walk through my recent work rebuilding VST on top of Iris, from the basic concept of memory ownership to the user-level tactics.

Speakers

William Mansky

Assistant Professor of Computer Science, UIC

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.

Related News & Events

simulated Roblox chat
UChicago CS News

Helping Elementary School Children Learn About Digital Privacy and Security With Micro-Lessons

Mar 25, 2025
grant ho writing on white board
UChicago CS News

New Study Reveals Gaps in Common Types of Cybersecurity Training

Mar 24, 2025
headshot
UChicago CS News

Jasmine Lu on Sustainable Computing: Rethinking E-Waste and Innovation

Mar 18, 2025
Pedro giving speech
UChicago CS News

Pedro Lopes Honored with 2025 IEEE VGTC Virtual Reality Significant New Researcher Award

Mar 13, 2025
ai generated network traffic
UChicago CS News

University of Chicago Researchers Revolutionize Network Traffic Generation with AI Breakthrough

Mar 12, 2025
UChicago CS News

Federal budget cuts threaten to decimate America’s AI superiority—and other countries are watching

Feb 25, 2025
Netflix logo on phone screen
UChicago CS News

The Hidden Cost of Netflix’s Autoplay: A Study on Viewing Patterns and User Control

Feb 25, 2025
Raul Castro Fernandez
UChicago CS News

Raul Castro Fernandez among six UChicago scientists awarded prestigious Sloan Fellowships in 2025

Feb 18, 2025
UChicago CS News

Quantum Leap: New Research Reveals Secrets of Random Quantum Circuits

Feb 04, 2025
UChicago CS News

Fred Chong from the Department of Computer Science Named ACM Fellow for Contributions to Quantum Computing

Jan 22, 2025
UChicago CS News

Rethinking AI as a Thought Partner: Perspectives on Writing, Programming, and More

Jan 16, 2025
UChicago CS News

UChicago Partners On New National Science Foundation Large-Scale Research Infrastructure For Education

Dec 10, 2024
arrow-down-largearrow-left-largearrow-right-large-greyarrow-right-large-yellowarrow-right-largearrow-right-smallbutton-arrowclosedocumentfacebookfacet-arrow-down-whitefacet-arrow-downPage 1CheckedCheckedicon-apple-t5backgroundLayer 1icon-google-t5icon-office365-t5icon-outlook-t5backgroundLayer 1icon-outlookcom-t5backgroundLayer 1icon-yahoo-t5backgroundLayer 1internal-yellowinternalintranetlinkedinlinkoutpauseplaypresentationsearch-bluesearchshareslider-arrow-nextslider-arrow-prevtwittervideoyoutube