Differences

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

--- comfusy [2010/03/24 20:49]
vkuncak
+++ comfusy [2013/10/16 18:27] (current)
mikael.mayer making-of added
@@ Line 1: / Line 1: @@
 ====== 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 ====
@@ Line 38: / Line 43: @@
                       ^
   answer: Int = 42
@@ Line 49: / Line 55: @@
   scalac -Xplugin:synthesis-plugin.jar -classpath synthesis-plugin.jar -P:synthesis:nowarnings YourFile.scala
-===== On YouTube =====
+(Comfusy parses Z3 models to produce a warning; versions of Z3 more recent than 2.18 may not output the proper format.)
-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]].
+===== 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 2010 Video]] (see the [[http://www.youtube.com/watch?v=a6uDAdhvpRE|making-of]] at 0:47).
-===== Reports =====
+===== People =====
-  * [[http://infoscience.epfl.ch/record/142733|Technical Report]]
+The people involved in the development of Comfusy are, in alphabetical order: [[http://lara.epfl.ch/~kuncak/|Viktor Kuncak]], [[http://people.epfl.ch/mikael.mayer|Mikaël Mayer]], [[http://icwww.epfl.ch/~piskac/|Ruzica Piskac]] and [[http://lara.epfl.ch/~psuter/|Philippe Suter]].