roadmap

ROADMAP

+
+= Roadmap for December 2010 =
+
+== Documentation ==
+
+* API: Andrei + Francois
+* tools: WhyML (JC), IDE (Claude
+* semantics: 
+* tutorial for API:
+** build a task
+** call a prover
+** apply a transformation
+** develop a new transformation
+
+== IDE ==
+
+(Claude)
+
+* database, session save and restore
+* Coq output
+* Gappa output
+
+== Misc ==
+
+* Builtin arrays in provers (Francois)
+* make install (done ?)
+* debug "make -j"
+* META for ocamlfind
+* headers
+
+
+
+= Roadmap for 2011 =
+
+* Jessie3
+* traceability
+* Coq plugin
+
+
+== Papers to write ==
+
+* Encodings and transformations (Andrei+Francois, CADE 2011, deadline January 2011)
+* Caml code ?
+* logic language for talking to provers
+** FOL + poly + alg + ind + rec ? + theories
+* VACID-0
+* system description (e.g. at CAD, TACAS)
+* rapports recherche ?