|
|
 |
 |
Dernière modification: 31.08.2009
Ce projet est maintenant terminé; il se poursuit avec FOST.
Ce projet est maintenant terminé; il se poursuit avec FOST.
- Transparents (en anglais) presentés à
la conférence ARITH-18:
"Formal Verification of Floating-Point programs".
- Nous avons formellement prouvé un programme calculant une récurrence
linéaire du second ordre. Vous pouvez voir le
programme C annoté ou télécharger le
programme C annoté accompagné de sa preuve
Coq.
- L'archive SVN.
- Version préliminaire du papier "Floats & Ropes: a
case study for formal numerical program verification" accepté
à la conférence ICALP.
- Version préliminaire du papier "Combining Coq and Gappa for Certifying Floating-Point Programs" accepté à la conférence Calculemus.