Georgios Giantamidis

Georgios Giantamidis · Mon, 04.01.2016

Attending the ExCAPE summer school on software synthesis was a very exciting experience. I was given the opportunity to meet in person and discuss with leading minds in my field of research, as well as view subjects I was already familiar with from a different perspective.

Since my research topic is learning in system design, the talks given by Sanjit Seshia were of particular interest to me. Sanjit defined formal inductive synthesis as an inductive learning problem and then proceeded to demonstrate how other important problems, including specification generation and verification, can be reduced to inductive synthesis. Afterwards, he presented CEGIS (Counter Example Guided Inductive Synthesis) a class of techniques that can be used to solve the inductive synthesis problem itself, and discussed its theoretical foundations.

While Sanjit focused on the theory behind CEGIS techniques, others presented, instead, interesting problem classes that can be solved using them. For example, Armando Solar-Lezama talked about syntax and template guided program synthesis, where the goal is to synthesize a program that, apart from having the desired behaviour, can also be derived by a given formal grammar or conforms to a given partially incomplete solution, respectively. Also, Steve Zdancewic talked about type directed program synthesis. In this setting, the search space is pruned by type information instead of syntactic structure information (as in the case of grammars and templates).

Other interesting sessions included Roderick Bloem's reactive synthesis tutorial, where I had the opportunity to refresh my knowledge on linear temporal logic and apply it to synthesize reactive systems using a tool called RATSY (Requirements Analysis Tool with Synthesis), as well as Vasumathi Raman's talk, where reactive synthesis was used to generate hybrid controllers (i.e. controllers having both discrete and continuous parts).