University of Toronto
Georgia Institute of Technology
Welcome to the Meel Group’s web page. Our group is based at the University of Toronto and the Georgia Institute of Technology.
Led by Kuldeep S. Meel, we develop scalable automated reasoning techniques that bridge theory and practice. Our research draws on randomized algorithms, statistical inference, formal methods, and distribution testing.
Our primary research interest is in automated reasoning. The long term vision of our research program is to advance automated reasoning techniques to enable computing to deal with increasingly uncertain real-world environments. The core theme of our research program is the quest for scalability. Accordingly, our work straddles theory and practice, and draws upon ideas from randomized algorithms, statistical inference, formal methods, distribution testing, and software engineering.
Our research spans multiple areas of computer science, as reflected in our publication record through 2026: artificial intelligence and machine learning (AAAI: 27×, IJCAI: 14×, NeurIPS: 6×, KR: 4×, AISTATS: 3×, ICML: 1×, ICLR: 1×), formal methods and constraint solving (CAV: 12×, SAT: 10×, CP: 9×, LPAR: 4×, TACAS: 3×), databases (PODS: 6×, ICDT: 2×), design automation (DAC: 3×, DATE: 3×, ICCAD: 2×), and theoretical computer science (LICS: 2×, SODA: 1×, ICALP: 1×, ESA: 1×). These connections allow us to bring advances in algorithms and reasoning systems to problems across disciplines.
Our 2026 publications include four journal articles and four conference papers on counting, sampling, synthesis, and verification.
Two of our papers were accepted to LPAR-26, held in Spetses, Greece, on October 25–30, 2026:
Our paper “Quantifying Sensitivity for Tree Ensembles: A Symbolic and Compositional Approach” (with Ajinkya Naik, Chaitanya Garg, S. Akshay, and Ashutosh Gupta) is accepted to CAV-26.
Our KR-25 paper received the Marco Cadoli Best Student Paper Award. Congratulations to our students, Arijit Shaw and Uddalok Sarkar.
Our paper “Provable Guarantees in Approximate Synthesis” (with Kushagra Gupta, Priyanka Golia, and Subhajit Roy) is accepted to DATE-26.
Our paper “The Limitations and Power of NP-Oracle-Based Functional Synthesis Techniques” (with Brendan Juba) is accepted to AAAI-26.
Our paper “Solution-Aware Vs Global ReLU Selection: Partial MILP Strikes Back for DNN Verification” (with Yuke Liao, Blaise Genest, and Shaan Aryaman) is accepted to ATVA 2025.
Our paper “Counting and Sampling Traces in Regular Languages” (with Alexis de Colnet and Umang Mathur) is accepted to POPL 2026.
Our group is based at the University of Toronto and the Georgia Institute of Technology. We work at the intersection of algorithm design and systems, with an emphasis on scalable automated reasoning. We welcome applicants with a strong background in algorithms, statistics, or formal methods and experience building research software.
Kuldeep plans to recruit 1–2 PhD students for Fall 2027. Please mention his name in your application and follow the application procedure of the institution you are applying to:
If you are a student at the University of Toronto or Georgia Tech and would like to discuss research opportunities, email Kuldeep to arrange a meeting.