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

UChicago CS News

Saturdays with CSIL — How Undergraduates are Transforming CS Education for Local High School Students

Dec 05, 2024
UChicago CS News

UChicago Researchers Receive Google Privacy Faculty Award for Research on AI Privacy Risks

Nov 22, 2024
UChicago CS News

The Climate App Designed to Tackle Chatham’s Flooding Crisis

Nov 21, 2024
In the News

Globus Receives Multiple Honors in 2024 HPCwire Readers’ and Editors’ Choice Awards

Nov 20, 2024
In the News

Argonne Team Breaks New Ground in AI-Driven Protein Design

Nov 15, 2024
UChicago CS News

DOE Awards Fred Chong and his National Research Team $7.5M to Develop a SMART Software Stack to Control Quantum Computer Noise

Nov 12, 2024
UChicago CS News

CS/LSSG Showcases Sustainability Research and Education

Nov 11, 2024
UChicago CS News

Ph.D. Student Jibang Wu Receives the Stigler Center Ph.D. Dissertation Award for His Work Modeling the Incentive Structures of Reward and Recommendation–Based Systems

Oct 24, 2024
UChicago CS News

Rebecca Willett Receives the SIAM Activity Group on Data Science Career Prize

Oct 23, 2024
UChicago CS News

UChicago CS Researchers Shine at UIST 2024 with Papers, Posters, Workshops and Demonstrations

Oct 10, 2024
UChicago CS News

UChicago Scientists Receive Grant to Expand Global Data Management Platform, Globus

Oct 03, 2024
UChicago CS News

UChicago Researchers Demonstrate the Quantifiable Uniqueness of Former President Donald Trump’s Language Use

Sep 30, 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