My goal is to develop tools using program synthesis and traditional compiler techniques to help developers and experts write optimal implementations.
Database Entity Resolution using Program Synthesis
We synthesize entity matching rules from positive and negative examples and show that our techniques can solve this problem using less data and involve less effort from the experts than the state of the art approaches. The core of this project is program synthesis, a powerful tool to quickly and automatically generate rules (or programs) from a rich generic grammar that provably satisfy the specification provided by given examples.
Automatic generation of SMT Solvers: SWAPPER, SAT Encoders
This project aims to automatically generate optimal versions of various parts of an SMT solver tuned to a particular domain of problems. SWAPPER is a framework for finding recurring patterns in formulas and automatically generating domain-specific rewriters used inside SMT solvers including the Sketch Synthesis system. The generated problem rewriters are auto-tuned to performance of the solver for problems from a particular domain. This idea was extended to automatic generation of optimal SAT encoders inside SMT solvers as well.
Bellmania is a framework allowing domain experts to manipulate computational terms in the interest of deriving better, more efficient implementations. It employs deductive reasoning to generate provably correct efficient implementations from a very high-level specification of an algorithm, and inductive constraint-based synthesis to improve automation. Semantic information is encoded into program terms through the use of refinement types.
Modular Program Synthesis in Sketch
This project combines constraint-based synthesis techniques with modular reasoning and demonstrates how to model various parts of your specification in this framework and efficiently solve them. This approach is implemented over the Sketch synthesis system.
Quantitative Synthesis of Reactive Systems and Concurrent Data-structures
This project solves quantitative synthesis problems modeled as two player games with probabilistic assumptions on the environment (Reactive systems) or model of the scheduler (Concurrent data-structures). This work includes two novel algorithms and their implementations for efficiently solving game-theoretic program synthesis problems.