Research

Foundations of Learning and Decision-Making

I use formal methods to develop foundations for reinforcement learning and sequential decision-making, including stochastic games and agents with differing time preferences. This work extends beyond finite-state, episodic settings to richer temporal objectives, recursive environments, and continuous-time physical systems.

• Reinforcement learning with temporal and omega-regular objectives
• Regular languages, automata, and reward machines
• Recursive and branching decision processes
• Continuous-time and physically grounded reinforcement learning
• History-dependent and nonstandard discounting models

Representative work:

• Regular Reinforcement Learning — CAV, 2024 · CAV Distinguished Paper Award
• Recursive Reinforcement Learning — NeurIPS, 2022
• Omega-Regular Objectives in Model-Free Reinforcement Learning — TACAS, 2019
• Continuous-Time Reward Machines — IJCAI, 2025

Verification for Learning and Control

Learning-enabled controllers must operate safely even when their environments are uncertain and their learned models are imperfect. I develop certificates, abstractions, and runtime mechanisms that connect formal verification with learning and control.

• Barrier, Lyapunov, and closure certificates
• Formal abstractions and simulation relations
• Safe transfer between learned controllers
• Runtime monitoring and shielding for reinforcement learning
• Safety-critical applications, including medical devices and cardiac control

Safe reinforcement learning for cardiac pacing, including the use of cardiac digital twins to evaluate pacing strategies, is an active research direction.

Representative work:

• Stochastic Neural Simulation Relations for Control Transfer — NeuS, 2025 · DARPA Disruptive Idea Award
• Closure Certificates — HSCC 2024

Accountable AI and Software

When software affects legal, financial, medical, or social outcomes, failures must be detectable and decisions must be open to scrutiny. I develop formal and data-driven methods for testing, explaining, and improving AI-driven software when complete specifications are unavailable.

This program also studies how learning and large language models can be combined with logic, automata, program analysis, and symbolic solvers to produce reasoning that is structured and auditable rather than merely plausible.

• Fairness testing and discrimination discovery
• Metamorphic and relational testing
• Neurosymbolic reasoning and proof-guided explanation
• Regulatory and legal accountability
• Explanation of sequential and combinatorial reasoning

Representative work:

• Fairness Testing through Extreme Value Theory — ICSE, 2025
• Uncovering Discrimination Clusters: Quantifying and Explaining Systematic Fairness Violations — ASE 2025
• Metamorphic Testing and Debugging of Tax Preparation Software — ICSE-SEIS 2023
• Explaining Hitori Puzzles: Neurosymbolic Proof Staging for Sequential Decisions — arXiv, 2025
• Explaining Puzzle Solutions in Natural Language: An Exploratory Study on 6x6 Sudoku — Findings of ACL, 2025