Colloquium Details
Software Synthesis using Automated Reasoning
Speaker: Ruzica Piskac, École Polytechnique Fédérale de Lausanne
Location: Warren Weaver Hall 1302
Date: May 17, 2011, 10:30 a.m.
Host: Clark Barrett
Synopsis:
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. I will describe how to generalize decision procedures into predictable and complete synthesis procedures using linear integer arithmetic as an example. Linear integer arithmetic is interesting in of itself due to the fact that reasoning about collections, such as sets and multisets, can be reduced to reasoning about linear integer arithmetic. The reduction uses a semilinear set characterization of solutions to integer linear arithmetic formulas and a generalization of a recent result on sparse solutions of integer linear programming problems. I will explain how this decision procedure can be applied in both software synthesis and program verification.
Speaker Bio:
Ruzica Piskac is a PhD candidate at EPFL, working under the supervision of Viktor Kuncak. Her primary research interests are decision procedures, their combinations and applications in program verification and software synthesis. She holds a Master's degree in Computer Science, obtained at the Max-Planck Institute for Computer Science in Saarbruecken, Germany and a Dipl.-Ing. degree in mathematics from the University of Zagreb, Croatia.
Notes:
In-person attendance only available to those with active NYU ID cards.