CS Colloquium
December 10, 2012
4:00 p.m., AKW 200

Host: Paul Hudak

Title: Software Synthesis using Automated Reasoning
Speaker: Ruzica Piskac, Max Planck Institute for Software Systems

Abstract: Software synthesis is a technique for automatically generating code from a given specification. The goal of software synthesis is to make software development easier while increasing both the productivity of the programmer and the correctness of the produced code. In this talk I will present an approach to synthesis that relies on the use of automated reasoning and decision procedures. First I will describe how to generalize decision procedures into predictable and complete synthesis procedures. Here completeness means that the procedure is guaranteed to find code that satisfies the given specification. I will illustrate the process of turning a decision procedure into a synthesis procedure using linear integer arithmetic as an example. In addition, I will outline a procedure that synthesizes code snippets from specifications implicitly given in the form of type constraints. As there can be multiple solutions, more than one code snippet can be a good candidate. We use an additional weight function to rank the derived snippets and direct the search for them. In practical evaluation, our technique scales to programs with thousands of visible declarations in scope and succeeds in 0.5 seconds to suggest program expressions of interest. I will conclude with an outlook on possible future research directions and applications of synthesis procedures. I believe that in the future we can make programming easier and more reliable by combining program analysis, software synthesis, and automated reasoning.


Bio: Ruzica Piskac is a tenure-track faculty member at the Max Planck Institute for Software Systems (MPI-SWS) and head of the Synthesis, Analysis and Automated Reasoning Group. Her research interests span the areas of software verification, automated reasoning, code synthesis and program termination. A common thread in Ruzica's research is improving software reliability and trustworthiness using formal techniques. Prior to joining MPI-SWS, she was a graduate student at the EPFL (2007-2011), where she worked under the supervision of Viktor Kuncak. She was awarded the Patrick Denantes Memorial Prize for her dissertation. She holds a Master's degree in Computer Science, obtained at the Max-Planck Institute for Computer Science in Saarbruecken, Germany. She also holds a Dipl.-Ing. Degree in mathematics from University of Zagreb, Croatia.