• Paper on Starling: Callback Typestates for Android Classes [pdf] was accepted at ICSE 2018. This work is about the automated learning of callin/callback protocols from android framework classes. Our implementation discovered several unknown bugs and corner cases in the android framework.
• Paper on Scaling Enumerative Program Synthesis via Divide and Conquer [pdf] was accepted at TACAS 2017. The paper contains a full description of a novel, efficient algorithm for the Syntax-Guided Synthesis problem.
• I presented preliminary results on the Synthesis of Interface Specifications for Android Classes at the IBM PL day 2016. This work is about the automated learning of asynchronous typestate for android framework classes. Our implementation discovered several unknown bugs in the android framework. Technical report can be found here.
• EUSolver (built by Abhishek Udupa and me) performed exceedingly well in the Syntax-guided Synthesis (SyGuS) competition 2016, winning the "general" and "programming-by-examples" track. EUSolver combines enumerative techniques for program synthesis [Udupa et. al. PLDI 2013] with unification [CAV 2015].
• Roopsha Samanta and I presented a tutorial on Trace-based Synchronization Synthesis for Concurrent Programs at POPL 2016. The tutorial will cover a large part of our work on synthesis for concurrency from the past few years.
• Recent and upcoming service:
  • CAV 2018: Program Committee.
  • CAV 2017: Program Committee.
  • SYNT 2017: Program Committee.
  • (EC)2 2016: Program Committee.
  • SYNT 2016: Program Committee.
  • CAV 2016: External Reviewing Committee.
  • PLDI 2016: External Reviewing Committee.

• Performance-aware Synthesis for Concurrency. Usable concurrency synthesis has been a long-standing goal, with over three decades of active research going into it. Here, a programmer is expected to write a program that is correct in a sequential context, and the synthesizer inserts sufficient synchronization (locks) to make the program behave correctly in a concurrent setting. However, the issue of performance of the synthesized program has not been fully addressed. In this project, we attempt to address this issue by both optimizing the synchronization inserted by the synthesizer, and by avoiding synchronization completely by using more "programmer-like" techniques.
• Quantitative Specifications for Reactive Systems. In this project, we attempt to construct a quantitative specification framework for analysis of reactive systems. Our framework is built on a novel notion called simulation distances. A simulation distance measures some aspect of "match" of a given system with respect to a property. The "match" could be anything including a measure of correctness (how often the system violates the property) or robustness (how much can the system be externally disturbed before it violates the property). We give algorithms to synthesize optimal systems with respect to this quantitative specifications.

The goal of formal methods has long been to produce software or hardware systems with provable guarantees on correctness. However, not all correct systems are equally desirable and not all incorrect systems are equally undesirable. In many cases, the notion of desirability of a system can be encoded as a quantity. Example of such quantities include execution time and energy consumption. My dissertation develops techniques for formal verification and synthesis for such quantitative specifications.

My dissertation was awarded the 2014 ACM SIGBED Paul Caspi Memorial Dissertation Award. The award is presented annually to the author of an outstanding dissertation in the area of Embedded Systems to recognize work that significantly advances the state of the art in the science of embedded systems, in the spirit and legacy of Dr. Paul Caspi's work.