home.md

@@ -9,9 +9,9 @@ Our main focus is to ensure that if the operation succeeds, the resulting progra
 Supported operations :
 
 *  Renaming global variables.
-** And swapping two global variable names.
+   * And swapping two global variable names. 
 *  Removing unused local variables.
-** And adding a local variable.
+   * And adding a local variable.
 
 
 # Status 
@@ -22,26 +22,31 @@ This is a proof of concept. It has the limitations given below.
 
 
 *  The research report is available at https://hal.archives-ouvertes.fr/hal-01248121 : *A Correct Refactoring Operation to Rename Global Variables in C Programs* (2015)
-*  An [article](http://arxiv.org/abs/1607.02226) was presented at the _4th International Workshop on Verification and Program Transformation_ (available in [Electronic Proceedings in Theoretical Computer Science](http://eptcs.web.cse.unsw.edu.au/content.cgi?VPT2016) / apr. 2016).
+*  An [article](http://arxiv.org/abs/1607.02226) was presented at the _4th International Workshop on Verification and Program Transformation_ (available in [Electronic Proceedings in Theoretical Computer Science](http://eptcs.web.cse.unsw.edu.au/content.cgi?VPT2016) / apr. 2016). *Renaming Global Variables in C Mechanically Proved Correct*
 * Another research report : *Memory bijections: reasoning about exact memory transformations induced by refactorings in CompCert C* : https://hal.archives-ouvertes.fr/hal-02078356/ (2019)
 
 # Limitations
 
-*  We do not take the preprocessor into account.
-*  We do not take comments and layout into account.
-*  We transform single files (we do not take the whole project into account).
-*  The proof of correctness does not cover the whole tool, only its core development in Coq.
+*  Our proofs of correctness cannot take the preprocessor into account.
+*  Our prototype cannot preserve comments, layout and preprocessing directives.
+*  Some parts of the tool (the driver) are written directly in OCaml and cannot be taken into account by proofs of correctness.
+
 
 # Development
 
-Developped by Julien Cohen, Lina laboratory ([Ascola team](http://www.emn.fr/z-info/ascola/doku.php) and now Galinette team), University of Nantes (Polytech Nantes). Igor Zhirkov is also working on this project.
+Developped by Julien Cohen, Lina laboratory (Ascola team http://www.emn.fr/z-info/ascola/doku.php), University of Nantes (Polytech Nantes).
+The operation that removes an unused local variable is developped by Igor Zhirkov.
+
 
 # What's new ?
 
-### Next Version
+### Version 0.7 (based on CompCert 2.7.1)
+
+* New refactoring operation : add/remove a local variable, by Igor Zhirkov.
+* Proof of correctness for renaming global variables is better structured.
+   *  Correspondences between semantic constructions in programs (contexts, continuations, states...) are now represented by relations and not by functions anymore. Proofs are easier, in particular for context transformation, which needed a painful encoding before, and for continuation transformation, which was too memory and time consuming. 
+   *  More iterators are used to ditinguish properties coming from renaming and those coming from tree traversals.
 
-* Based on Compcert 2.7 (for compatibility).
-* More understandable proofs.
 
 ### Version 0.6 (based on Compcert 2.6)