I am an Assistant Professor in the Department of Computer Science at Purdue University. I lead the Purdue Formal Methods (PurForM) group and am a member of the Purdue Programming Languages (PurPL) group. Before joining Purdue in 2016, I completed my PhD at UT Austin in 2013, advised by E. Allen Emerson and Vijay K. Garg, and was a postdoctoral researcher at IST Austria from 2014-2016 with Thomas A. Henzinger. I am a recipient of a 2019 NSF CAREER award and a 2021 Amazon Research Award.
My research interests are in program verification, program synthesis, and concurrency. I like to work at the intersection of formal methods and programming languages to assist both programmers and non-programmers write programs that conform to their intent. I am actively seeking motivated and talented graduate students and postdoctoral researchers. If you wish to work with me, email me with a statement explaining your interest in my research.
||Modular, Bounded Verification of Unbounded Distributed Systems. Modern distributed services are typically built in a modular fashion using core distributed protocols as building blocks. The ubiquity of some of these building blocks has sparked several valiant verification efforts for them in the last decade. Oddly, there have been far fewer verification efforts that go beyond core protocols and target distributed services built on top of such core protocols. In our ambitious Discover[i] project (pronounced, disovery), we seek to develop modular, scalable, fully-automated verification approaches for distributed systems that mimic their modular design. In particular, we advocate an approach based on assuming that the underlying core protocols are verified separately and encapsulating their complexities within cleanly-defined abstractions. See this talk or read our OOPSLA'21 QuickSilver paper and our CAV'20 paper to learn more.|
||Semantics-Guided Inductive Program Synthesis. Example-based program synthesis and repair are increasingly favored paradigms of program synthesis as they can help democratize programming. Because examples and other inductive specifications are inherently incomplete, inductive synthesis engines encounter challenges such as overfitting, ambiguity, and brittleness, similar to inductive learning-based engines. PL researchers have typically attacked these problems by applying syntactic biases to the search space in the form of tailored DSLs, grammars and ranking functions. We are exploring a variety of techniques to further enhance the generalizability and robustness of such engines by applying semantic biases to the search space. Check out our CAV'16 Qlose paper and PLDI'19 SemCluster paper targeting semantics-guided program repair, and our POPL'20 paper targeting semantics-guided program synthesis.|
|Sep'21||Excited about my talk on our MANTIS project at Strange Loop on Oct 1. This will be my first in-person talk since the COVID-19 pandemic broke out!|
|Sep'21||Looking forward to my invited talk on our Discover[i] project at the DISC Workshop on Formal Reasoning in Distributed Algorithms (FRIDA) on Oct 8!|
|Sep'21||QuickSilver will appear in OOPSLA 2021!|
|Jul'21||Delighted and honored to receive an Amazon Research Award!|
|Jul'21||Our next Discover[i] work — QuickSilver: A Modeling and Parameterized Verification Framework for Systems with Distributed Agreement — with Nouraldin Jaber, Christopher Wagner, Swen Jacobs, and Milind Kulkarni conditionally accepted to OOPSLA 2021!|
|Dec'20||Enjoyed giving a keynote on our MANTIS project at the NeurIPS Workshop on Computer-Assisted Programming!||All posts|
|Program Synthesis: A Dream Realized?
|Augmented Example-based Synthesis using Relational Perturbation Properties.
|Discover[i]: Component-based Parameterized Reasoning for Distributed Applications.
MSR, Redmond, 2018.
|Computer-aided Concurrent Programming.
Papers We Love Conference, 2018.