- 6
- 1
Guillaume Melquiond
7
Documents
Publications
- 3
- 2
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 7
- 4
- 3
- 3
- 3
- 3
- 3
- 2
- 1
- 1
- 1
- 1
- 1
- 3
- 1
- 1
|
|
Trusting computations: a mechanized proof from partial differential equations to actual programComputers & Mathematics with Applications, 2014, 68 (3), pp.28. ⟨10.1016/j.camwa.2014.06.004⟩
Article dans une revue
hal-00769201v3
|
|
|
Wave equation numerical resolution: a comprehensive mechanized proof of a C programJournal of Automated Reasoning, 2013, 50 (4), pp.423-456. ⟨10.1007/s10817-012-9255-4⟩
Article dans une revue
hal-00649240v3
|
|
|
Preserving User Proofs Across Specification ChangesFifth Working Conference on Verified Software: Theories, Tools and Experiments, May 2013, Atherton, United States. pp.191-201
Communication dans un congrès
hal-00875395v1
|
|
|
Formal proof of a wave equation resolution scheme: the method errorITP'10 - Interactive Theorem Proving, Jul 2010, Edinburgh, United Kingdom. pp.147-162, ⟨10.1007/978-3-642-14052-5_12⟩
Communication dans un congrès
inria-00450789v3
|
|
|
Combining Coq and Gappa for Certifying Floating-Point Programs16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Jul 2009, Grand Bend, Ontario, Canada. pp.59-74, ⟨10.1007/978-3-642-02614-0_10⟩
Communication dans un congrès
inria-00432726v1
|
Why3 version 1.0France, N° de brevet: IDDN.FR.001.420003.000.S.P.2019.000.20600. 2018
Brevet
hal-03136256v1
|
|
|
The Why3 platform 0.812013
Autre publication scientifique
hal-00822856v1
|