REFACCERT: Research report is out with a new release !

Added by Julien COHEN over 2 years ago

A research report on refactoring in Compcert C is now available at . The corresponding code is available here in the Files tab, release "Research report hal-01248121 version 1".

What's new in that release ?

  • We show the preservation of the set of possible behaviors (terminates, diverges, reacts forever, goes wrong).
  • We give a sufficient precondition and several forward and backward description for static composition.

REFACCERT: First version is out !

Added by Julien COHEN over 2 years ago

The first version of RefacCert is out.

You can download the sources in the "Files" or "Fichiers" tab.

We provide an operation that renames global variables. The correctness (bisimulation) of the core operation is proven.

The limitations of the tool are described on the wiki tab.

The hypotheses necessary for the correctness are described in Correctness.v .

Also available in: Atom