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.
- Won first prize in PLDI SRC 2015 and ACM SRC grand finale 2016 in Undergrad category (Poster
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".
- 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
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
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.