Changeset 1436 for Deliverables/D4.2-4.3
- Timestamp:
- Oct 21, 2011, 5:27:16 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.2-4.3/reports/D4-2.tex
r1435 r1436 433 433 These axiomatised components are found in the ERTL to LTL pass. 434 434 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. 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. Therefore, we plan to provide implementations in OCaml only, 436 and to provide certified verifiers in Matita. At the moment, the implementation 437 of the certified verifiers is left as future work. 436 438 \item 437 439 \textbf{A few non-computational proof obligations.}
Note: See TracChangeset
for help on using the changeset viewer.