Ruzica Piskac is a PhD candidate at EPFL, working under the
supervision of Viktor Kuncak. Her primary research interests
are program verification and software synthesis based on automated
reasoning. She holds a Master's degree in Computer
Science, obtained at the Max-Planck Institute for Computer
Science in Saarbruecken, Germany. Her Master's thesis advisor was
Harald Ganzinger and the topic of her thesis was formal
verification of a priority queue checker using first-order
theorem provers. She also holds a Dipl.-Ing. degree in
mathematics from University of Zagreb, Croatia. Prior to her PhD
studies at EPFL, Ruzica worked at the Digital Enterprise Research
Institute in Innsbruck, where she was involved in several
EU-funded projects on large-scale automated reasoning to support
intelligent data access on the web (LarCK, SEKT, RW2). Ruzica
received a Google Anita Borg memorial scholarship in 2010.

SWS, RG1   Info

Expert Audience

English

60 Minutes

Kaiserslautern

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. Next I will outline a synthesis procedure for
specifications given in the form of type constraints. The
procedure takes into account polymorphic type constraints as well
as code behavior. The procedure derives code snippets that use
given library functions. 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.

Maria-Louise Maggio

0631-93039600

--email hidden

Yes

Saarbrücken

E1 5

5th floor

passcode not visible

logged in users only