Speaker: Bohan Li
Abstract: SMT has been widely applied in software analysis, verification, and testing. This talk focuses on SMT problems over arithmetic theories, where the mainstream solving paradigm is the DPLL(T) framework. However, DPLL(T) relies heavily on the interaction between SAT and theory solvers, leading to significant performance degradation when handling complex theories. While local search has achieved notable success as an incomplete method for SAT, its extension to arithmetic-theory SMT remains largely unexplored due to inherent technical challenges. Exploring how to integrate local search techniques into SMT on arithmetic theories and achieve performance competitive with mainstream approaches is therefore of great interest. Moreover, existing SMT solvers rely on abundant computational resources and memory, while the proliferation of terminal devices poses new challenges for solver design in terms of real-time performance and lightweight implementation. This report discusses local search algorithms for arithmetic-theory SMT and their applications in terminal environments.
Bio: Bohan Li is an assistant professor at the Institute of Artificial Intelligence for Industries, Chinese Academy of Sciences. He received his Ph.D. degree from the Institute of Software, Chinese Academy of Sciences, in 2025. His research interests focus on the solving and application of Satisfiability Modulo Theories (SMT). He has published over 10 papers in leading international conferences and journals such as CAV, FM, ICSE, ToCL, CP, and IJCAI, and has won multiple championships in international SMT competitions. He has been awarded the CAS President Award and was selected for the Outstanding Ph.D. Dissertation Award of CCF Formal Methods Committee.