Distribution Testing: The New Frontier for Formal Methods

Abstract:  The dominant guiding philosophy in the first sixty years of Computer Science was for designers to design systems that were always correct, and to accept nothing less as users. But times have changed: Users and designers are accustomed to systems with statistical components and behaviors. What does it mean for the formal methods community? In this talk, we argue that such a dramatic change in the acceptance and design of systems presents exciting opportunities to make fundamental contributions: we need to rethink the notions and techniques for the design of specifications and verification methodologies. In particular, we will focus on the systems whose behaviors are not naturally captured by symbolic relations but rather require reliance on probability distributions. We will discuss our recent efforts in designing formal methodologies for testing whether a sampling subroutine generates a desired distribution. We will showcase the challenges, opportunities, and rewards in our journey.

Speaker Bio:  Kuldeep Meel holds Stephen Fleming Early-Career Associate Professorship in the School of Computer Science, and an Associate Professor at the University of Toronto (on leave). His research interests lie at the intersection of Formal Methods and Artificial Intelligence. He is a recipient of the 2022 ACP Early Career Researcher Award, the 2019 NRF Fellowship for AI, and was named AI’s 10 to Watch by IEEE Intelligent Systems in 2020. His research program’s recent recognitions include the Distinguished Paper Award at CAV-23 and CAV-24, ICLP-24 Best Paper Award,2023  CACM Research Highlight Award, 2022 ACM SIGMOD Research Highlight, IJCAI-22 Early Career Spotlight,  Best Paper Award nominations at ICCAD-21 and DATE-23, 1st Place in Model Counting Competition (2020 and 2022).  He is passionate about teaching, and most proud of being recipient of university-level Annual Teaching Excellence Awards in 2022 and 2023.