Changeset 1437 for Deliverables/D4.2-4.3


Ignore:
Timestamp:
Oct 21, 2011, 5:30:06 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.2-4.3/reports/D4-2.tex

    r1436 r1437  
    488488We plan to validate the backend translations, removing any obvious bugs, by executing the translation inside Matita on small C programs.
    489489This is not critical, as the certification process will find all bugs anyway.
     490\item We plan to provide certified validators for all results provided by
     491external oracles written in OCaml. At the moment, we have axiomatized oracles
     492for computing least fixpoints during liveness analysis, for colouring
     493registers and for branch displacement in the assembler code.
    490494\end{itemize}
    491495
Note: See TracChangeset for help on using the changeset viewer.