This is an old revision of the document!

====== Working Group 4 on Synthesis ====== **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. * Efficient implementations of synthesis algorithms using not only binary decision diagrams but also quantified (Boolean) formulas, and the development of benchmarks for synthesis problems within the Rich Model benchmark suite from Working Group 1. * Quantitative generalization of synthesis, including: extending Boolean specifications by quantitative measures in order to rank implementations by laziness, fairness, or parsimonious use of resources, non-Boolean algorithms that generalize decision procedures from Working Group 2, and quantitative games as a method for solving synthesis problems. * Simplified synthesis problems of practical interest, including problems with limited quantifier alternations, using synthesis for problems where some part of the structure is predefined (e.g., repair, sketching). * Using synthesis to implement high-level programming language constructs. 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. ====== Research on Synthesis within and outside of the action ====== 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. ===== Synthesizers from Linear Temporal Logic (LTL or LTL-like) Specifications ===== Here is an incomplete list of people and tools on the topic of synthesis from linear temporal logic specifications. * [[http://www.iaik.tugraz.at/content/research/design_verification/|TU-Graz, IAIK-D&V]] (Roderick Bloem, Georg Hofferek, Robert Könighofer) **Tools**: ([[http://www.iaik.tugraz.at/content/research/design_verification/lily/|Lily]], [[http://www.iaik.tugraz.at/content/research/design_verification/anzu/|Anzu]],) [[http://rat.fbk.eu/ratsy/|Marduk]] (part of Ratsy) * [[https://es.fbk.eu/index.php|FBK Trento, Embedded Systems Research Unit]] (Alessandro Cimatti, Marco Roveri, Viktor Schuppan, Stefano Tonetta) **Tool:** [[https://es.fbk.eu/index.php?n=Tools.NuGaT|NuGat]] (used as backend in Ratsy) * [[http://react.cs.uni-sb.de/|University of Saarbrücken, Reactive Systems]] (Bernd Finkbeiner, Rüdiger Ehlers) **Tool:** [[http://react.cs.uni-sb.de/tools/unbeast/|Unbeast]] * [[http://www.ulb.ac.be/di/verif/index-en.html|University Libre Bruxelles, Formal methods and verification group]] (Jean-François Raskin), **Tool**: [[http://www.antichains.be/acacia/papers.html|Acacia]] * [[http://www-verimag.imag.fr/~jobstman/|Verimag Grenoble (Barbara Jobstmann)]] **Tools:** ([[http://www.iaik.tugraz.at/content/research/design_verification/lily/|Lily]], [[http://www.iaik.tugraz.at/content/research/design_verification/anzu/|Anzu]],) [[http://pub.ist.ac.at/quasy/|Quasy]] * [[http://rsg.informatik.uni-kl.de/|University Kaiserlautern, Embedded Systems Group]] (Klaus Schneider, Andreas Morgenstern) * [[http://users.ics.tkk.fi/kepa/|Aalto University (Keijo Heljanko)]] * CU University (Fabio Somenzi) * Weizmann Institute of Science ([[http://ysaar.net/|Yaniv Saar]], [[http://en.wikipedia.org/wiki/Amir_Pnueli|Amir Pnueli]]) and University of Leicester ([[http://www.cs.le.ac.uk/people/npiterman/|Nir Piterman]]) **Tools:** [[http://www.wisdom.weizmann.ac.il/~saar/synthesis/|GR1-Synthesizer]] Notes on a [[synthesis:ltlformat|common format for LTL synthesis]]. ===== Other Game Solvers ===== * [[https://es.fbk.eu/index.php?n=Tools.NuGaT|NuGat]] (FBK Trento) * [[http://www6.in.tum.de/~chengch/gavs/|GAVS+]] (TUM, Fortiss) * [[http://pub.ist.ac.at/gist/index.html|GIST]] (IST Austria, Verimag Grenoble) * [[http://www2.tcs.ifi.lmu.de/pgsolver/|pgsolver]] (LMU, University of Kassel) * [[http://www.cs.aau.dk/~adavid/tiga/|UPPAL-TIGA]] Solver for timed games * [[http://automata.rwth-aachen.de/research/GASt/|GasT]] (RWTH Aachen) not maintained anymore ===== Synthesizers for Sequential Code, Code-Snippets, or Synchronization ===== * [[http://lara.epfl.ch/w/impro|EPFL, LARA]] (Viktor Kuncak) **Implicit programming** * [[http://research.microsoft.com/en-us/um/people/sumitg/pubs/synthesis.html|Microsoft Research (Redmond Lab), RiSE Group]] (Sumit Gulwani) * [[http://groups.csail.mit.edu/cap/|MIT Computer-Aided Programming (CAP) Group]] (Armando Solar-Lezama) **Program Sketching** * [[http://www.cs.berkeley.edu/~bodik/|UC Berkeley]] (Rastislav Bodik) **Program Sketching** * [[http://www.cs.technion.ac.il/~yahave/|Technion (Eran Yahav)]] **Synthesizing Synchronizations** * [[http://gadara.eecs.umich.edu/|University of Michigan, EE and CS]] (Stéphane Lafortune) **Gadara: Orchestrating the execution of parallel programs using Discrete Control Theory** * [[http://sites.google.com/site/galkatzzz/mcgp-tool|MCGP Tool]] (Doron Peled and Gal Katz) **Automatic generation and correction of programs using Genetic Programming** * [[http://AspectLTL.ysaar.net)|AspectLTL]] (Yaniv Saar and Shahar Maoz) **a temporal-logic based language for the specification and implementation of crosscutting concerns.** * [[http://users.soe.ucsc.edu/~luca/papers/05/emsoft05.pdf|Code Aware Resource Management]] ([[https://sites.google.com/a/ucsc.edu/luca/home|L. de Alfaro]], [[http://people.na.infn.it/~mfaella/|M. Faella]], [[http://www.cs.ucla.edu/~rupak|R. Majumdar]], V. Raman)