The field of automated programming envisions a software design process where programmers write partial, nondeterministic specifications of programming tasks, and powerful program synthesis algorithms are used to find correct implementations of these specifications. In this talk, I will describe my recent work in this area. Topics covered will include:
- Smoothed proof search, a program synthesis technique that is based on the construction of a series of "smooth" approximations to a program's abstract semantics.
- The use of automated fixpoint computation techniques, such as counterexample-guided refinement and logical abduction, in the synthesis of infinite-state software.
- Synthesis across abstraction boundaries – in particular, a method for synthesizing robotics code that unites reasoning at the discrete task level and the continuous physical level.
Swarat Chaudhuri is an assistant professor of computer science at Rice University. He is an expert on program verification and synthesis. Swarat received his Ph.D. in computer science from the University of Pennsylvania in 2007. He is a recipient of the National Science Foundation CAREER award and the ACM SIGPLAN Outstanding Doctoral Dissertation Award.
Faculty Host: Umut Acar