Date: September 10, 2026
Time: 11:45 a.m. - 12:45 p.m.
Location: G01 Gates Hall
Title: Gradual Verification: Usable and Incremental Software Assurance
Speaker: Jonathan Aldrich, Carnegie Mellon University
Host: Saikat Dutta
Abstract: AI coding agents accelerate software production but risk introducing more bugs and vulnerabilities. New formal verification tools, type systems, and safe languages like Rust promise to mitigate these risks. However, moving these into industrial practice is challenging: large existing codebases exist and cannot be immediately rewritten or verified, and the power of these new tools often compromises their usability. We are developing gradual verification to address the software engineering reality that technology adoption must be usable and incremental. While traditional work in programming languages has treated usability at best in an informal way, we find that formal user studies can identify barriers to the adoption of these new technologies as well as identify and validate ways to overcome them; our results show substantial benefits to productivity and correctness. While traditional verification is viewed monolithically, our gradual verification approach enables engineers to focus on the properties and modules that are most critical to their applications. Gradual verification benefits from both new theoretical insights about how to build verification tools as well as systems research hybridizing static and dynamic checking. I'll illustrate these ideas through our ongoing BorrowSanizer project checking interoperation between safe Rust and unsafe C/C++ code, among others.
Bio: Jonathan Aldrich is a Professor of Computer Science and Software Engineering at Carnegie Mellon University, where he directs the Master of Software Engineering program. He is the coauthor (with Michael Scott) of the textbook Programming Language Pragmatics, 5th edition. His research combines programming languages, software engineering, and human-computer interaction to explore how the way we express software affects our ability to engineer software at scale. A particular theme of much of his work is improving software quality and programmer productivity through better ways to express structural and behavioral aspects of software design within source code. Aldrich has contributed to ownership, typestate checking, modular and gradual verification techniques, and usability in programming language and type system design. For his work specifying and verifying architecture, he received a 2006 NSF CAREER award, the 2007 Dahl-Nygaard Junior Prize, and an ICSE test of time award. Outside the university, he serves on ACM Council and was the CTO of Noteful, a startup delivering an educational app for music theory and note reading.
