Hi, this is John Lü 吕正旸. Welcome to my personal webpage!

I am a 4th-year PhD student in Computer Engineering at UWaterloo, supervised by Vijay Ganesh and Arie Gurfinkel. My research focuses on formal verification, with applications in both software and hardware systems.

News

• [Sep 2025] I completed a 4-month research internship at NII, working on Probabilistic Program Verification. Many thanks to my host Ichiro Hasuo for the wonderful guidance and support!
• [May 2025] Our paper Btor2-Select: Machine Learning Based Algorithm Selection for Hardware Model Checking is accepted to CAV 2025!
• [May 2025] Honored to receive NSERC CGS-D, a top-tier Canadian federal PhD scholarship.
• [Feb 2025] I co-organized and presented the AAAI’25 tutorial ML for Solvers! You can check the slides and materials on our website.
• [Nov 2024] I successfully completed my Google Summer of Code project! Many thanks to my GSoC mentors Po-Chun Chien and Nian-Ze Lee from LMU Munich. During this project, we developed the first ML-based algorithm selector for the Btor2 hardware verificaiton problem.
• [Sep 2024] I start serving as the ECE-GSA Co-Chair for the upcoming year.
• [Aug 2024] Our paper Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis is presented at IJCAI 2024! Super grateful to Kate Larson for help us present this research!
• [Jul 2024] At SMT 2024, I made my first paper presentation (with crutches)!
• [Jul 2024] Our solver Z3-alpha won multiple awards at SMT-COMP 2024! It excelled across divisions such as QF_Datatypes, QF_LinearIntArith, QF_NonLinearIntArith, and QF_NonLinearRealArith! Read more on Georgia Tech News.
• [May 2024] Attended the inaugural AI-SCORE Summer School and had so much fun!
• [Sep 2023] 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.