Updates

Our research on predicting laptop user experience, with colleagues in chromeOS org at Google, was selected for a poster and oral presentation at the NeurIPS 2023 workshop on ML for Systems.

We present regression-based models for predicting ChromeOS user experience metrics from hardware specifications of Chromebook laptops.

Our work on automated analysis of AWS IoT Events Detector Models, with colleagues in the Automated Reasoning Group (ARG) at Amazon Web Services AWS, would appear at CAV 2023 for publication in the Springer-Verlag LNCS series.

We present a collection of automated analyzers that help AWS customers verify that their IoT Event detector models are free of common defects.

We released the third iteration of the syntax-guided synthesis (SyGuS) language standard at SYNT 2021. The major extensions in the SyGuS 2.1 Standard include support for oracles (contributed by Elizabeth Polgreen), a new CHC_X logic (that generalizes the previous Inv_X logic, contributed by me), and a new theory of tables (contributed by Andrew Reynolds and Chenglong Wang).
The 2021 SyGuS competition was postponed, but we would be adding corresponding new competition tracks in the 2022 competition.

Another patent, with the PROSE group at Microsoft on dataset sampling using program synthesis, was granted (after 4 years)!

Our work on ILP-guided invariant synthesis, with colleagues in the Systems group at Microsoft Research Lab (India), was selected for a poster presentation at the NeurIPS 2020 workshop on Computer-Assisted Programming.

We present a new approach to synthesizing provably sufficient loop invariants by leveraging integer linear programming (ILP).

My work on data-driven inference of representation invariants, with Anders Miltner and Prof. David Walker at Princeton University and my advisor Prof. Todd Millstein, would appear at PLDI 2020.

We present a counterexample-driven algorithm to infer provably sufficient representation invariants that certify correctness of data-structure implementations. Our implementation, Hanoi, can automatically infer representation invariants for several common recursive data structures, such as sets, lists, trees, etc.

My first patent, with the PROSE group at Microsoft on data profiling using program synthesis, was granted! USPTO seems super backlogged — our application was pending for over two years.

My work investigating overfitting in SyGuS, with my advisor Prof. Todd Millstein, Aditya Nori, and Rahul Sharma, would appear at CAV 2019 for publication in the Springer-Verlag LNCS series.

We define overfitting in the context of CEGIS-based SyGuS, and show that there exists a tradeoff between expressiveness and performance. We present two mitigation strategies: (1) a black-box approach that any existing tool can use, and (2) a white-box technique called hybrid enumeration.

An extended version of my undergraduate thesis work on slicing functional programs, with Prasanna Kumar, Prof. Amey Karkare and my then-advisor Prof. Amitabha Sanyal, would appear at CC 2019.

We propose a static analysis for slicing functional programs, which precisely captures structure-transmitted dependencies and provides a weak form of context sensitivity — weakened to guarantee decidability. We also show an incremental version this technique that is efficient in practice.

My research on pattern-based profiling, with PROSE group (at Microsoft) and my advisor Prof. Todd Millstein, would appear at SPLASH-OOPSLA 2018 for publication in the PACMPL journal.

We present a technique, called FlashProfile, to generate hierarchical data profiles. Existing tools, including commercial ones, generate a single flat profile, and are often overly general or incomplete. Furthermore, we show that data profiles can improve accuracy and efficiency of PBE techniques.

My research on data-driven precondition inference, with Rahul Sharma and my advisor Prof. Todd Millstein, would appear at PLDI 2016.

We present a technique, called the precondition inference engine (PIE), which uses on-demand feature learning to automatically infer a precondition that would satisfy a given postcondition. We use PIE to also construct a novel automatic verification system called LoopInvGen.