Organizers: Ras Bodik (University of Washington), Radu Grosu (TUWien), Ruzica Piskac (Yale University), Sanjit Seshia (University of California, Berkeley)
The workshop aims to bring together researchers interested in the broad area of synthesis of computational models and systems. Software controls an increasingly large part of infrastructure and cyber-physical systems (CPSs), such as sensors, cars and datacenters. On the one hand, we therefore need to automate software development as much as possible, which is facilitated by model-based design. On the other hand, we need to automate model and system creation, as well as its adaptation and repair.
The synthesis problem refers to the collection of algorithmic techniques that automatically construct software artefacts (models, controllers, programs) from specifications or behavioural observations. The specifications are usually stated in a logical formalism and can be quantitative, and behavioural observations include examples of inputs and outputs and time series data. One advantage of synthesis is that it yields an artefact that is correct by construction, which avoids the need to fix the bug once it has been found using verification. An issue with synthesis is that it does not have a canonical statement of the problem, which has given rise to a variety of approaches, each characterised by the type of inputs considered: reactive synthesis, template-based program synthesis, controller synthesis from (quantitative) temporal logic specifications, syntax-guided synthesis, counter-example guided inductive synthesis, assume-guarantee component synthesis, and parameter synthesis. An emerging area is program synthesis and repair using machine learning, which encompasses automata learning and the use of deep and reinforcement learning.
The research area of synthesis has seen great progress in the past decade, stemming from novel algorithms and progress in neighboring areas such as constraint solving, game theory and planning.
The workshop will build on these advances and will aim to build connections between different subareas of synthesis: from program synthesis and model synthesis to methods based on machine learning. The challenging problem areas that are synthesis for networks and distributed systems are the primary target applications.
All events take place in the Calvin Lab auditorium.
Further details about this workshop will be posted in due course. Enquiries may be sent to the organizers tfcs2021 [at] lists [dot] simons [dot] berkeley [dot] edu (at this address).