People

Our group studies the theoretical foundations and practical applications of trustworthy artificial intelligence. We emphasize mathematical rigor, clear reasoning, and problems motivated by consequential real-world systems, including cyber-physical systems and software used in legal and societal decision-making.

We are part of the Programming Languages and Verification (CUPLV) group at CU Boulder.

Current group members

Research collaborators

• John Komp

PhD students

• David Baines (since Fall 2022) — Reinforcement learning for finance
• Alireza Nadali (since Fall 2022) — Transfer learning for control
• Amin Falah (since Spring 2023) — Reinforcement learning for continuous-time MDPs
• Lekai Chen (since Fall 2023; co-advised with Alvaro Velasquez) — Large language models and formal languages

How we work

Our research is shaped by regular technical discussions, careful reading and writing, and a strong emphasis on foundational understanding. Group members are encouraged to develop intellectual independence while engaging deeply and constructively with one another’s work.

Most of our projects combine theoretical ideas with systems-oriented thinking. We value precise problem formulation, clear exposition, and thoughtful feedback. Our broader goal is to help researchers develop the technical depth, independence, and judgment needed to pursue important long-term research questions.

Join the group

I welcome inquiries from prospective PhD students and postdoctoral researchers interested in formal methods, reinforcement learning, cyber-physical systems, and AI accountability. Strong theoretical foundations and curiosity about real-world impact are particularly valuable.

If you are interested in joining the group, please send me a concise email describing your background, research interests, and how they connect with our work. Prospective PhD students should also consult the CU Boulder Computer Science graduate admissions page.

Group life through the years

Alumni

PhD alumni

• Saeid Tizpaz-Niari (PhD 2020) — Faculty, University of Illinois Chicago
• Devendra Bhave (PhD 2020) — Principal Software Engineer, MathWorks
• Tianhan Lu (PhD 2023) — Research Scientist, Meta
• Taylor Dohmen (PhD 2024) — AI Research Scientist, 3M
• John Komp (PhD 2024)
• Vishnu Murali (PhD 2024) — Postdoctoral Researcher, CU Boulder
• Mateo Perez (PhD 2025) — Founder and CEO, Jazzberry
• Shadi Tasdighi-Kalat (PhD 2025) — VP of Research, Unveer

MS and BS thesis advisees

• Miles Zheng (undergraduate thesis)
• Saksham Srivastava — “LLMs and Program Synthesis”
• Jordan Perr-Sauer (MS, Summer–Fall 2022) — “Verification of Neural Networks”
• Zachary Mckevitt (BS, Fall 2020–Spring 2022) — “RNNs for Automatic Transient-Execution Attack Detection”
• Vishnu Murali (MS, 2019–2020) — “Optimal Repair for Omega-Regular Properties”; continued into the PhD program

MS and BS research advisees

• Aaptha Boggaram — Artificial cardiac pacemakers and AI
• Varsha Dewangan — Technical challenges in maintaining tax-preparation software with LLMs
• Ali Almutawa Jr. (BS, Summer 2022; co-advised with Fabio Somenzi)
• Adam Adl (BS, Summer 2022; co-advised with Fabio Somenzi)
• Ian Mckibben (BS, Summer 2021; co-advised with Fabio Somenzi)
• Emily Millican (BS, Spring 2020) — Embedded Software Engineer, Ball Aerospace
• John Paul Martin (MS, 2018–2020; co-advised with Evan Chang)
• Juraj Culak (MS, 2017–2019)
• Mateo Perez (BS, Summer 2018–Spring 2020; co-advised with Fabio Somenzi) — Founder and CEO, Jazzberry
• Shemal Somil Lalaji (MS, Fall 2019) — Visa
• Capstone Team “Love Bugs” (ECEE self-driving-car project; co-advised with Fabio Somenzi): Mohammed Al Hasani, George Matthew Helmick, Rodolfo Gonzalez Hill V, Myungshin Im, Michael Shea Oliver, and Mateo Perez
• Aniruddha Phatak (MS/PhD, 2019–2020; co-advised with Pavol Cerny)
• Aniket Lata (MS, 2015–2016; co-advised with Evan Chang) — Qualcomm
• Ram Das Diwakaran (MS, 2016–2017; co-advised with Sriram Sankaranarayanan) — Generac

Academic genealogy

Explore my academic ancestry — a complete graph of the advisor relationships recorded in the Mathematics Genealogy Project, with searchable names, highlighted paths, and a downloadable poster.