Hi, this is John Lü (吕正旸 in Chinese). Welcome to my person website!

I am a 2nd-year PhD student at the University of Waterloo, Canada, under the supervison of Prof. Vijay Ganesh and Prof. Arie Gurfinkel. I also have a long-time collaration with Prof. Florin Manea’s research group at the Universty of Göttingen since 2021.

My research interests lie at the intersection of machine learning and formal methods. Some projects that I am currently working on include:

• Algorithm Selection and Strategy Synthesis for SMT
• Algorithm Selection for Verification
• String Constraint Solving
• Machine Learning for SAT heuristics

News

• Jul 2024 Our solver Z3-alpha won multiple awards at SMT-COMP 2024 (Single Query Track)! It achieved first place in QF_NonLinearIntArith and QF_NonLinearRealArith and had the best UNSAT-performance in QF_Datatypes and the best SAT-performance in QF_LinearIntArith.
• Jul 2024 I will serve as the Co-Chair of the ECE Gradudate Student Association (ECEGSA) for the upcoming year. I’m excited to contribute to the community and help foster a supportive environment for fellow graduate students.
• Jun 2024 Happy to receive the Winter 2024 Faculty of Engineering (FOE) Graduate Scholarship at UWaterloo.
• May 2024 Attended the inaugural AI-SCORE Summer School and had so much fun!
• May 2024 Our IJCAI 2024 paper Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis is accepted at SMT 2024 for presentaiton-only. See you in Montreal in July!
• Apr 2024 Honored to be accepted as a Google Summer of Code (GSoC 2024) contributor, working with the SoSy-Lab at LMU Munich. The accepted project is titled Adaptive Algorithm Selection for Btor2 Verification Tasks.
• Apr 2024 Our paper Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis is accepted at IJCAI 2024! See you in Jeju Island in August.
• Sep 2023 Happy to start working as the Website Chair for CAV 2024.
• Jul 2023 Offcially start my PhD journey at UWaterloo! Thanks for the generous funding from the Engineering Excellence Doctoral Fellowship (EEDF) and the Deans Entrance Award.
• Jun 2023 Check my recently accepted UWaterloo MASc thesis AlphaSMT: A Reinforcement Learning Guided SMT Solver.