*** NOTE the special time and place ***
Friday April 22 3:00 - 4:15 PM Kelley 1007 Sumit Gulwani Researcher Microsoft Research Synthesis of Loop-Free Programs We consider the problem of synthesizing loop-free programs that implement a desired functionality using components from a given library. Specifications of the desired functionality and the library components are provided as logical relations between their respective input and output variables. We solve the component-based synthesis problem using a constraint-based approach that involves first generating a synthesis constraint, and then solving the constraint. The synthesis constraint is a first-order \exists\forall logic formula whose size is quadratic in the number of components. We present a novel algorithm for solving such constraints. Our algorithm is based on counterexample guided iterative synthesis paradigm and uses off-the-shelf SMT solvers. We present experimental results that show that our tool "Brahma" can efficiently synthesize highly nontrivial 10-20 line loop-free bitvector programs. These programs represent a state space of approximately 2010 programs, and are beyond the reach of the other tools based on sketching and superoptimization. Biography Sumit Gulwani is a researcher in the RiSE group at Microsoft Research, Redmond. His primary research interest is in the area of program synthesis with applications to automating end user programming and building automated tutoring systems. Sumit obtained his PhD in computer science from UC-Berkeley in 2005, and was awarded the C.V. Ramamoorthy Award and the ACM SIGPLAN Outstanding Doctoral Dissertation Award. He obtained his BTech in computer science and engineering from the Indian Institute of Technology (IIT) Kanpur in 2000 and was awarded the President's Gold Medal. _______________________________________________ Colloquium mailing list [email protected] https://secure.engr.oregonstate.edu/mailman/listinfo/colloquium
