From Decision Procedures to Synthesis Procedures

Vortrag im Kolloquium Informatik von Dr. Ruzica Piskac (Yale University), Montag, 09.01, 14:00 Uhr (s.t.), Raum B 233

Referent: Dr. Ruzica Piskac (Yale University)

Gastgeber: Prof. Dr. Viorica Sofronie-Stokkermans


Title: From Decision Procedures to Synthesis Procedures


Automated reasoning is concerned with the design of theorem provers and decision procedures, which are an enabling technology for increasing software reliability.

In this talk we present the first decidable logic for reasoning about multisets with cardinality constraints. Such constraints naturally arise in software verification, e.g., for programs that implement or use container data structures. We then show how to generalize decision procedures into predictable and complete synthesis procedures.

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.


We outline how to broaden usability and applications of current software synthesis techniques. We conclude with an outlook on possible future research directions and applications of synthesis procedures.



Dr. Ruzica Piskac is an assistant professor (tenure-track) at Yale, Computer Science Department. Her research interests span the areas of programming languages, software verification, automated reasoning, and code synthesis. A common thread in Ruzica's research is improving software reliability and trustworthiness using formal techniques. Ruzica has received a NSF CAREER award for her proposal, "Synthesis in a Live Programming Environment".  She proposed the concept of cooperative programming which combines a live programming environment and the programming by example paradigm.

Wann 09.01.2017
von 14:00 bis 16:45
Termin übernehmen vCal