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/19 17:04]
jobstman
synthesis [2011/12/21 14:04] (current)
barbara.jobstmann
Line 15: Line 15:
  
 Below we give an incomplete list of pointers to research within and outside the action related to this working group. Below we give an incomplete list of pointers to research within and outside the action related to this working group.
-(UNDER CONSTRUCTION)+This is list under construction. Feel free to extend it.
  
 ===== Synthesizers from Linear Temporal Logic (LTL or LTL-like) Specifications ===== ===== Synthesizers from Linear Temporal Logic (LTL or LTL-like) Specifications =====
Line 24: 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)
Line 31: Line 31:
   * 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]]   * 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 48: 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)