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

I am a 2nd-year PhD student at the University of Waterloo. My supervisors are Prof. Vijay Ganesh and Prof. Arie Gurfinkel. I am also collarbating with Prof. Florin Manea’s group at the Universty of Göttingen and Prof. Dirk Beyer’s group at LMU Munich.

My strongest research interest is to combine reasoning and learning. Below are some of my active research projects:

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

News

• [Nov 2024] Together with collarabtors from Geogia Tech and UBC, I’m organizing an AAAI’25 tutorial ML for Solvers! More info will be posted on our website. Hope to see you in Philadelphia!
• [Nov 2024] From May to November, I successfully completed a Google Summer of Code project! Many thanks to my GSoC mentors Po-Chun Chien and Dr. Nian-Ze Lee from LMU Munich. During this project, we developed the first ML-based algorithm selector for the Btor2 hardware verificaiton prroblem. I will be presenting some early results at the AAAI’25 Student Program.
• [Sep 2024] I start serving as the ECE-GSA Co-Chair of the upcoming year. I’m excited to contribute to the community and help foster a supportive and inclusive environment for fellow graduate students. Let me know if you have any ideas or suggestions for initiatives or events you’d like to see this year!
• [Aug 2024] Our paper Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis is presented at IJCAI 2024! Unfortunately, I couldn’t travel to Jeju Island due to a broken ankle, but I’m super grateful to Prof. Kate Larson for help us present this research! This research was partly developed during Kate’s CS686 class as a course project, and her feedback along the way was incredibly helpful. Thank you so much, Kate!
• [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.
• [Jun 2024] Happy to receive the Winter 2024 FOE Graduate Scholarship! Some more bucks to enjoy a decent dinner : )
• [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.