Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
synthesis [2011/04/13 18:09] jobstman |
synthesis [2011/12/21 14:04] (current) barbara.jobstmann |
||
---|---|---|---|
Line 11: | Line 11: | ||
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. | 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. | ||
- | ===== Synthesizers from Linear Temporal Logic (LTL or LTL-like) Specifications ===== | ||
- | (UNDER CONSTRUCTION) | + | ====== 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. | Here is an incomplete list of people and tools on the topic of synthesis from linear temporal logic specifications. | ||
Line 20: | Line 24: | ||
* [[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) | * [[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://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|Akazia]] | + | * [[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://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://rsg.informatik.uni-kl.de/|University Kaiserlautern, Embedded Systems Group]] (Klaus Schneider, Andreas Morgenstern) | ||
* [[http://users.ics.tkk.fi/kepa/|Aalto University (Keijo Heljanko)]] | * [[http://users.ics.tkk.fi/kepa/|Aalto University (Keijo Heljanko)]] | ||
* CU University (Fabio Somenzi) | * CU University (Fabio Somenzi) | ||
- | * Weizmann Institute of Science (Yaniv Saar, Armir Pnueli) and University of Leicester (Nir Piterman) **Tools:** [[http://www.wisdom.weizmann.ac.il/~saar/synthesis/|GR1-Synthesizer]] | + | * 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 ===== | ===== Other Game Solvers ===== | ||
- | * [[http://automata.rwth-aachen.de/research/GASt/|GasT]] (RWTH Aachen) | + | * [[https://es.fbk.eu/index.php?n=Tools.NuGaT|NuGat]] (FBK Trento) |
* [[http://www6.in.tum.de/~chengch/gavs/|GAVS+]] (TUM, Fortiss) | * [[http://www6.in.tum.de/~chengch/gavs/|GAVS+]] (TUM, Fortiss) | ||
* [[http://pub.ist.ac.at/gist/index.html|GIST]] (IST Austria, Verimag Grenoble) | * [[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://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://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 ===== | ===== Synthesizers for Sequential Code, Code-Snippets, or Synchronization ===== | ||
Line 44: | Line 51: | ||
* [[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://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://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://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) |