P. Madhusudan - University of Illinois at Urbana-Champaign
Students: Spring 2024, unless noted otherwise, sessions will be virtual on Zoom.
The Role of Automata Theory in Software Verification
Oct 27, 2010
Download: MP4 Video Size: 451.1MBWatch on YouTube
Abstract
The 80s and 90s saw a revolution in hardware verification, where automata theory played a prominent role, formalizing model-checking and establishing the basis of verification using the logic-automata connection. We shift focus to software verification and ask how exactly would automata theory be useful in program analysis.Drawing from work in recent years in software verification in my research group as well as in the field, I will identify several key areas, ranging from modeling, abstraction, model-checking, interface synthesis, testing, to logical reasoning with dynamic data-structures, where automata theory promises to provide the right abstractions and yield effective tools for program analysis.
About the Speaker
Madhusudan worked for his Ph.D. at the Institute of Mathematical Sciences, India, and after a three-year post-doc stint at UPenn, joined the faculty at the Unviersity of Illinois at Urbana-Champaign. His research interests are primarily in the verification and analysis of software, with an emphasis on methods involving concurrency, logic and automata theory.