Special Talk

  • Gates Hillman Centers
  • ASA Conference Room 6115
  • Postdoc
  • Department of Electrical Engineering and Computer Sciences
  • University of California at Berkeley

Towards scalable program synthesis

The automatic generation of programs from non-executable specifications would have a tremendous impact on software engineering, and in particular would help to tackle security problems. However, with program synthesis methods being limited to a few lines of code at a time, we are still far away from usefulness. In this talk I will discuss fundamental problems with existing program synthesis algorithms, such as enumerative program synthesis and CEGIS, and suggest a new algorithmic principle to overcome these problems. For that we will resort to a simplified setting, quantified Boolean formulas (QBFs), where the suggested algorithm already significantly improves over the state of the art in terms of the number of solved instances, solving time, and the size of certificates. In the last part of the talk I will present some initial, promising experiments for program synthesis.

Markus N. Rabe is a postdoc at UC Berkeley, where he works with Prof. Sanjit Seshia. In his research he focuses on the fundamental aspects of program synthesis and security. His recent works include a completely new approach to quantifier elimination that tackles the scalability problem of program synthesis and an approximate probabilistic optimization algorithm to find inputs to programs that cause a worst-case leakage. In his PhD at Saarland University under the supervision of Prof. Bernd Finkbeiner he developed HyperLTL, a temporal logic capable of expressing a wide range of properties from information-flow control, and new model checking algorithms to automatically check information-flow properties for complex hardware systems.

Faculty Host: Jean Yang