[10]
|
Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela
Mayero, Guillaume Melquiond, and Pierre Weis.
Wave equation numerical resolution: Mathematics and program.
Research Report 7826, INRIA, December 2011.
[ bib |
full text on HAL ]
We formally prove the C program that implements a simple numerical scheme for the resolution of the one-dimensional acoustic wave equation. Such an implementation introduces errors at several levels: the numerical scheme introduces method errors, and the floating-point computation leads to round-off errors. We formally specify in Coq the numerical scheme, prove both the method error and the round-off error of the program, and derive an upper bound for the total error. This proves the adequacy of the C program to the numerical scheme and the convergence of the effective computation. To our knowledge, this is the first time a numerical analysis program is fully machine-checked.
Keywords: Formal proof of numerical program; Convergence of numerical scheme; Proof of C program; Coq formal proof; Acoustic wave equation; Partial differential equation; Rounding error analysis
|
[9]
|
François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei
Paskevich.
The Why3 platform, version 0.71.
LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.71 edition,
October 2011.
https://gforge.inria.fr/docman/view.php/2990/7635/manual.pdf.
[ bib ]
Keywords: Why3
|
[8]
|
Asma Tafat and Claude Marché.
Binary heaps formally verified in Why3.
Research Report 7780, INRIA, October 2011.
http://hal.inria.fr/inria-00636083/en/.
[ bib |
full text on HAL ]
Keywords: Why3
|
[7]
|
Krishnamani Kalyanasundaram and Claude Marché.
Automated generation of loop invariants using predicate abstraction.
Research Report 7714, INRIA, August 2011.
http://hal.inria.fr/inria-00615623/en/.
[ bib |
full text on HAL ]
|
[6]
|
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume
Melquiond, and Andrei Paskevich.
The Why3 platform.
LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.64 edition,
February 2011.
http://why3.lri.fr/.
[ bib ]
Keywords: Why3
|
[5]
|
Yannick Moy and Claude Marché.
The Jessie plugin for Deduction Verification in Frama-C ---
Tutorial and Reference Manual.
INRIA & LRI, 2011.
http://krakatoa.lri.fr/.
[ bib |
PDF |
http ]
|
[4]
|
Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier
Urbain.
Automated Certified Proofs with CiME3.
Technical Report 2044, Cédric laboratory, CNAM Paris, France, 2011.
[ bib |
.pdf |
Abstract ]
|
[3]
|
Thi Minh Tuyen Nguyen and Claude Marché.
Proving floating-point numerical programs by analysis of their
assembly code.
Research Report 7655, INRIA, 2011.
http://hal.inria.fr/inria-00602266/en/.
[ bib |
full text on HAL ]
|
[2]
|
Paolo Herms, Claude Marché, and Benjamin Monate.
A certified multi-prover verification condition generator.
Research Report 7793, INRIA, 2011.
http://hal.inria.fr/hal-00639977/en/.
[ bib |
full text on HAL ]
|
[1]
|
Catherine Lelay.
étude de la différentiabilité et de l'intégrabilité en
Coq : Application à la formule de d'Alembert pour l'équation des
ondes.
Master's thesis, Université Paris 7, 2011.
http://www.lri.fr/~lelay/Rapport.pdf.
[ bib ]
|