I am a second year PhD student in Computer Science at MIT advised by Prof. Armando Solar-Lezama. My research interests are in Program Synthesis and Formal Methods.

You can find my resume here.

  • WebRelate: Joining Web Data with Relational Data using Examples, Jeevana Priya Inala, and Rishabh Singh. Under submission.
  • Synthesis of Recursive ADT Transformers from Reusable Templates, Jeevana Priya Inala, Nadia Polikarpova, Xiaokang Qiu, Ben Lerner, and Armando Solar-Lezama. To appear in TACAS 2017. [arXiv]
  • Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers, Jeevana Priya Inala, MEng Thesis, MIT 2016 [pdf]
  • Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers, Jeevana Priya Inala, Rohit Singh, and Armando Solar-Lezama. SAT 2016, Bordeaux, France. [pdf]
  • Type-Aware Transactions for Faster Concurrent Code, Nathaniel Herman, Jeevana Priya Inala, Yihe Huang, Lillian Tsai, Eddie Kohler, Barbara Liskov, and Liuba Shrira. EuroSys 2016, London, UK.
  • Microsoft Research Women's Fellowship, 2016-17.
  • Charles and Jennifer Johnson MEng Thesis First Place Award, 2016.
  • First place in ACM SRC Grand Finale in Undergrad category, 2016.
  • First place in PLDI student research competition in Undergrad category, 2015.
  • Acitifio Undergrad Research and Innovation Scholar, 2014-15.
  • Gold Medal at 13th Asian Physics Olympiad, 2012 held in New Delhi, India.
  • Silver Medal and Asian Girl topper in 43rd International Physics Olympiad, 2012 held in Tallinn, Estonia.
  • Gold Medal and Best in Theory in 5th International Olympiad in Astronomy and Astrophysics, 2011 held in Krakow, Poland.
  • Silver Medal in 14th International Olympiad in Astronomy, 2009 held in Hangzhou, China.
Numerical Synthesis

We are developing a tool to reason about both discrete and continuous components of hybrid systems more efficiently than existing approaches. Given some boolean and real unknown parameters and a specification (logic constraints), the goal of the tool is to find a setting to these unknown parameters that satisfies the specification. We have applied the technique to two different applications in autonomous driving -- 1. To synthesize control programs that provably satisfy safety properties and 2. To learn traffic models for driving behaviors from real driving data sets so that formal analysis can take realistic traffic into account.

SyntRec - Won first prize in PLDI SRC 2015 and ACM SRC grand finale 2016 in Undergrad category (Poster) (Slides)

We implemented a system called SyntRec that helps implement interesting functions involving pattern matching and algebraic data types. One of the novel aspects of this work is the combination of type inference and counterexample-guided inductive synthesis (CEGIS) in order to support very high-level notations for describing a space of possible implementations. We also come up with a new encoding for synthesis problems involving immutable data-structures that significantly improves the scalability. The approach is evaluated on a set of case studies which most notably include synthesizing desugaring functions for lambda calculus that force the synthesizer to discover Church encodings for pairs and boolean operations, as well as a procedure to generate constraints for type inference.


STO is a software transactional memory (STM) based not on low-level reads and writes on memory, but on datatypes-arrays, lists, queues, hash tables, and so forth-that explicitly support transactional op- erations. In a conventional, untyped STM, transaction bookkeeping uses read and write sets of memory words, and even simple requests can generate many more transactional memory accesses than the minimum necessary to ensure correctness. Our insight is that concurrent data structures can generate fewer superfluous accesses, and use more efficient concurrency protocols, when transaction bookkeeping tracks high-level operations like "insert node into tree".

OptCNF - Won Charles and Jennifer Johnson MEng Thesis First Place Award (Slides)

The theory of bit-vectors in SMT solvers is very important for many applications due to its ability to faithfully model the behavior of machine instructions. A crucial step in solving bit-vector formulas is the translation from high-level bit-vector terms down to low-level boolean formulas that can be efficiently mapped to CNF clauses and fed into a SAT solver. In this project, we demonstrate how a combination of program synthesis and machine learning technology can be used to automatically generate code to perform this translation in a way that is tailored to particular problem domains. Using this technique, we can improve upon the basic encoding strategy used by CVC4 (a state of the art SMT solver) and automatically generate variants of the solver tailored to different families of problems represented in the bit-vector benchmark suite from the SMT-COMP 2015 competition.

Concolic Execution for Django Applications (Writeup) (Code1) (Code2)

This is a 6.858 (Computer systems security) final project.
Concolic execution systems allow developers to verify that invariants in their applications are not violated no matter what input is given by a user. The idea is to use Z3 solver to find inputs that would trigger inconsistencies in web application. Unfortunately, there is no framework that would work for general web applications especially those that are implemented in Django. Invariant checking is useful for a wide range of applications, and thus we built a generic concolic execution interface for any Django-based web application.

Joint work with Luke Anderson, Jon Gjengset and Andrew Wang.

Learning with Wasserstein Loss in Caffe (Writeup)

This is a 6.867 (Machine Learning) final project.
Implemented a regularized Wasserstein loss layer in Caffe. Used it to perform supervised learning on MNIST datasets and image segmentation tasks.

Joint work with Prafulla Dhariwal.