Event Actions
Verification’s Last Mile Problem (And How to Solve It In The Age of AI)
Abstract:
We have the tools to formally guarantee software correctness, yet most software engineers don't use them. The reason isn't (only) ignorance; it's economics: the programs we care about are large and already exist, and it is too expensive to manually adapt them just to satisfy a verifier. This talk presents a three-pronged research agenda to automate this adaptation process and finally make verification practical. First, we reimagine type inference not as a passive annotation task, but as an active, human-like refactoring process. Our system automates the tedious work of both adding types and making code changes to satisfy the typechecker—from fixing latent bugs to navigating the tool's limitations. Second, we address the classic problem of scale: many verification techniques work well on small examples, but not full-size programs. We've developed a program reduction technique that allows a verifier to be "indirectly" applied to a massive program by identifying and analyzing a tiny, provably-relevant subprogram. Finally, we’ll look forward to how generative artificial intelligence can be harnessed to automate the journey to provably-reliable code.
About the Speaker:
Martin Kellogg is an assistant professor of computer science at the New Jersey Institute of Technology (NJIT). His PhD from the University of Washington, where was advised by Michael Ernst; he also has a BS in Computer Science from UVa (wahoowa!). His research focuses on making software verification practical for every developer: that is, on making verification a standard part of every developer’s toolkit, in the way that techniques like unit testing or code review are today. His focus is primarily on two approaches to making verification more practical: 1) improving the expressivity of simple verification technologies: making it possible to prove more facts about a program within the constraints that developers actually work under, and 2) convincing developers of the benefits of verification: by deploying verification technologies in new domains, and by improving the usability of verification. For example, Kellogg has developed new, more practical verification techniques that guarantee the absence of security vulnerabilities caused by malformed object initialization, array bounds errors that might lead to buffer overflow attacks, and denial-of-service attacks against web servers caused by resource leaks. Verification tools based on his work that prove properties related to security, compliance, and program correctness have been deployed at large technology companies, including Amazon Web Services. His work has been published in prestigious venues including ICSE, ESEC/FSE, ASE, ISSTA, and OOPSLA, and has been generously supported by the NSF.