Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
|
comfusy [2010/03/31 16:36] philippe.suter |
comfusy [2012/12/19 14:37] philippe.suter |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== COMFUSY: COMplete FUnctional SYnthesis ====== | ====== COMFUSY: COMplete FUnctional SYnthesis ====== | ||
| - | Comfusy works as a plugin for the [[http://scala-lang.org|Scala]] compiler. Comfusy was developed and tested with the version 2.7.7 of Scala (not the recent 2.8 release). | + | Comfusy is a tool for synthesizing executable code from specifications in linear integer arithmetic and constraints on sets of objects. |
| + | * see [[http://lara.epfl.ch/~kuncak/papers/KuncakETAL10CompleteFunctionalSynthesis.html|PLDI 2010 Paper]] for the description of this work | ||
| - | * You can download the .jar file of the plugin here: [[http://lara.epfl.ch/~psuter/comfusy/synthesis-plugin.jar|synthesis-plugin.jar]] (older version: [[http://lara.epfl.ch/~psuter/comfusy/synthesis-plugin-older.jar|synthesis-plugin-older.jar]], without support for parametrized linear integer arithmetic) | + | Comfusy works as a plugin for the [[http://scala-lang.org|Scala]] compiler. Comfusy was developed and tested with the version 2.7.7 of Scala (*not* the more recent 2.8.* or 2.9.* releases). |
| + | |||
| + | * You can download the .jar file of the plugin here: [[http://lara.epfl.ch/~psuter/comfusy/synthesis-plugin.jar|synthesis-plugin.jar]] (older version: [[http://lara.epfl.ch/~psuter/comfusy/synthesis-plugin-older.jar|synthesis-plugin-older.jar]], without support for parametrized linear integer arithmetic). | ||
| + | |||
| + | * The source code is [[https://github.com/epfl-lara/comfusy|available on GitHub]] for the brave. | ||
| ==== Examples ==== | ==== Examples ==== | ||
| Line 38: | Line 43: | ||
| ^ | ^ | ||
| answer: Int = 42 | answer: Int = 42 | ||
| + | |||
| Line 48: | Line 54: | ||
| * You can disable these checks by compiling the code with the command: | * You can disable these checks by compiling the code with the command: | ||
| scalac -Xplugin:synthesis-plugin.jar -classpath synthesis-plugin.jar -P:synthesis:nowarnings YourFile.scala | scalac -Xplugin:synthesis-plugin.jar -classpath synthesis-plugin.jar -P:synthesis:nowarnings YourFile.scala | ||
| + | |||
| + | (Comfusy parses Z3 models to produce a warning; versions of Z3 more recent than 2.18 may not output the proper format.) | ||
| ===== On YouTube ===== | ===== On YouTube ===== | ||
| Comfusy has been used to synthesize a part of computation used to generate the following [[http://www.youtube.com/watch?v=E2aPFdu0FNA|Happy New Year Video]]. | Comfusy has been used to synthesize a part of computation used to generate the following [[http://www.youtube.com/watch?v=E2aPFdu0FNA|Happy New Year Video]]. | ||
| - | |||
| - | |||
| - | ===== Reports ===== | ||
| - | |||
| - | * [[http://infoscience.epfl.ch/record/142733|Technical Report]] | ||
| ===== People ===== | ===== People ===== | ||