Changeset 1436 for Deliverables


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

...

File:
1 edited

Legend:

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

    r1435 r1436  
    433433These axiomatised components are found in the ERTL to LTL pass.
    434434
    435 It should be noted that these axiomatised components fall into the following pattern: whilst their implementation is complex, and their proof of correctness is difficult, we are able to quickly and easily verify that any answer that they provide is correct.
     435It should be noted that these axiomatised components fall into the following pattern: whilst their implementation is complex, and their proof of correctness is difficult, we are able to quickly and easily verify that any answer that they provide is correct. Therefore, we plan to provide implementations in OCaml only,
     436and to provide certified verifiers in Matita. At the moment, the implementation
     437of the certified verifiers is left as future work.
    436438\item
    437439\textbf{A few non-computational proof obligations.}
Note: See TracChangeset for help on using the changeset viewer.