Differences

This shows you the differences between two versions of the page.

Link to this comparison view

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-likeSpecifications =====
  
 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)