Commit 0c00a03b authored by MARCHE Claude's avatar MARCHE Claude

roadmap for 2011

parent 43c9f637
= Roadmap for second release, as early as possible in 2011 =
* fix local installation
* ajouter "invalid" comme cas de resultats de preuve
* utiliser call_provers.proof_result dans gmain
* file names in DB
** use only file names relative to the db file
** ou alors interdire d'avoir plusieurs fichiers dans la meme base
* proof replay
** in IDE
** in whybench
** add replay of existing proofs in "make bench" to detect regression
= Roadmap for 2011 =
* WhyML (JC)
* Jessie3
* traceability
* Coq plugin
* Coq realizations of theories
= 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 ?
= Roadmap for December 2010 =
== Documentation ==
......@@ -168,35 +219,3 @@ using the Why3 public discussion list and bug tracker.
= Roadmap for second release, as early as possible in 2011 =
* file names in DB
** use only file names relative to the db file
* proof replay
** in IDE
** in whybench
** add replay of existing proofs in "make bench" to detect regression
= Roadmap for 2011 =
* WhyML (JC)
* Jessie3
* traceability
* Coq plugin
* Coq realizations of theories
= 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 ?
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment