Topics of Interest: New algorithms for synthesis from high-level specifications. Extending decision procedures to perform synthesis tasks. Connections between invariant generation and code synthesis.
Working Group 4 explores the theory, tools, and usability of synthesis in system development. In contrast to automated verification algorithms, which establish whether a given system satisfies a given specification, synthesis algorithms automatically construct implementation that is guaranteed to satisfy a given specification. Synthesis is more difficult than verification, and is one of the holy grails of Computer Science. Despite impressive theoretical results of the past, it was only recently that researchers made significant steps towards the development of practical synthesis algorithms. Synthesis still has many limitations preventing its wider practical application. Working Group 4 aims to address these limitations through tasks that include the following. * Developing synthesis algorithms for more expressive logics, including identifying decidability and worst-case complexity of synthesis for expressive logics, developing heuristics and new subclasses of problems that overcome high complexity, lifting decision problems (explored in Working Group 2) to synthesis problems, developing high-level synthesis techniques applicable to components, and synthesis of hybrid systems.
Action experts have a unique set of complementary skills, whose combination will be necessary to fulfill the research vision of synthesis. By giving a more active role to automated tasks and avoiding low-level coding, synthesis has the potential to dramatically improve the productivity of computer system developers.
Below we give an incomplete list of pointers to research within and outside the action related to this working group. This is list under construction. Feel free to extend it.
Here is an incomplete list of people and tools on the topic of synthesis from linear temporal logic specifications.
Notes on a common format for LTL synthesis.