Conference Papers

PLDI ' 20
( )
Data-Driven Inference of Representation Invariants
Anders Miltner,  Saswat PadhiTodd MillsteinDavid Walker
⟬   ACM SIGPLAN Distinguished Paper ⟭  

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.

CAV ' 19
( )
Overfitting in Synthesis: Theory and Practice

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.

CC ' 19
( )
A Static Slicing Method for Functional Programs and Its Incremental Version
Prasanna Kumar K.,  Amitabha Sanyal,  Amey KarkareSaswat Padhi

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.

PLDI ' 16
( )
Data-Driven Precondition Inference with Learned Features
Saswat PadhiRahul SharmaTodd Millstein
⟬   Winner of SyGuS-Comp (Inv Track) 2017 – 18 ⟭  

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.

Journal Papers

( )
FlashProfile: A Framework for Synthesizing Data Profiles
Saswat PadhiPrateek Jain,  Daniel Perelman,  Oleksandr PolozovSumit GulwaniTodd Millstein

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.


In Preparation
( )
OASIS: ILP-Guided Synthesis of Loop Invariants
Sahil Bhatia,  Saswat Padhi,  Nagarajan Natarajan,  Rahul SharmaPrateek Jain

Reports & Theses

PhD Dissertation ' 20
( )

Patent Grants & Applications

Grant 2019
[ 10394874B2 ]
App. 2018
[ 20180121525A1 ]
Record Profiling for Dataset Sampling
Daniel G. Simmons,  Kevin D. J. Grealish,  Sumit Gulwani,  Ranvijay Kumar,  Kevin Michael EllisSaswat Padhi