Next Gen Automated Reasoning: Beyond “SAT Revolution” to “Beyond SAT” Revolution
10/02/2022, 2:30pm
Speaker
Abstract
The current generation of automated reasoning techniques excel at the qualitative tasks (i.e., when the answer is Yes or No) owing to the dramatic progress in satisfiability solving,also referred to as the SAT revolution. Such techniques sufficed to reason about traditional systems whose design sought to achieve deterministic behavior. In contrast, modern computing systems crucially rely on statistical methods to account for the uncertainty in the environment. To reason about the behavior of these systems in uncertain environments, there is a need to look beyond qualitative symbolic reasoning techniques.
In this talk, I will discuss the design of the next generation of automated reasoning techniques to perform higher-order tasks such as quantitative measurement (aka counting), sampling of representative behavior, and automated synthesis of systems. Naturally, these tasks are hard from a complexity-theoretic viewpoint, and therefore, our frameworks focus on tight integration of real-world applications, beyond the worst-case analysis algorithmic design and data-driven system design. This has allowed us to obtain breakthrough results in counting, sampling, and synthesis, providing a new algorithmic toolbox in formal methods, probabilistic reasoning, and design verification, and enabling the transition from Beyond “SAT Revolution” to “Beyond SAT” Revolution. I will discuss the core design principles and the utility of the above techniques on various real a pplications, including neural network verification, critical infrastructure reliability, quantitative information-flow analysis, and design verification.
Speaker Bio
Kuldeep Meel holds the NUS Presidential Young Professorship in the School of Computing at the National University of Singapore. His research interests lie at the intersection of Formal Methods and Artificial Intelligence. He is a recipient of the 2019 NRF Fellowship for AI, accompanied with USD 2 million funding, and was named AI’s 10 to Watch by IEEE Intelligent Systems in 2020. His work received the 2021 Amazon Research Award, the 2022 ACM SIGMOD Research Highlight, the 2018 Ralph Budd Award for Best Ph.D. Thesis in Engineering, the 2014 Outstanding Masters Thesis Award from Vienna Center of Logic and Algorithms, and Best Student Paper Award at CP 2015. His CP-18 paper, CAV-20, and PODS-21 papers received IJCAI-19 Sister conferences best paper award track invitation, “Best of PODS-21” invite from ACM TODS, and “Best Papers of CAV-20” invite from FMSD journal, respectively.