I'm a PhD candidate in the Siebel School of Computing and Data Science at the University of Illinois Urbana-Champaign. I'm fortunate to be advised by Prof. Sasa Misailovic. I work on formal methods, agentic AI and software engineering. Broadly, I'm interested in finding ways to ensure reliability of software systems (those comprised of AI agents and those generated using AI agents).
We observe tool-calling agents violating domain-specific policy (provided in the system prompt), even when using frontier models. Agent-C enforces formal temporal policies on the tool calls of agents, to prevent policy violations. Agent-C checks if there exists a finite satisfiable suffix to the trace of tool calls, at every step of the agent's tool usage. We evaluate on τ2-Bench and demonstrate improvements in safe utility and conformance of agents.
We study whether LLMs can supply inductive loop invariants for automated program verification. Loopy prompts an LLM for candidate loop invariants and ranking functions, then filters them with a Houdini-loop, which iteratively discards non-inductive clauses in the invariant (using a linear number of checker calls). Loopy infers correct invariants for 408/469 scalar-loop benchmarks. The symbolic baseline, Ultimate, verifies 430/469 benchmarks. Loopy and Ultimate together verify 461/469 benchmarks, hinting that combining symbolic tools with LLM-based techniques can improve the existing state-of-the-art.
MRDTs cast replicated data types in the mould of distributed version control. A purely functional data structure becomes replicated by equipping it with a three-way merge. Prior MRDTs verify only convergence, and their local operations are far slower than the sequential structures they replace. Peepul adapts an approach of using a replication-aware simulation relation to tie a data type's specification to its efficient implementation. We verify multiple MRDTs in F*, including the first formally verified replicated queue, and run them on Irmin.
ParaFuzz extends Crowbar (AFL-based grey-box fuzzing with QuickCheck) to Multicore OCaml programs. ParaFuzz mocks Multicore OCaml's parallelism API with an effect-handler scheduler that yields at every synchronisation point and lets AFL pick which thread runs next. It effectively explores the joint space of possible inputs and thread interleavings. The framework allows for deterministic replay of buggy thread schedule + input combination.