|
[20]
|
Clément Fumex, Claude Marché, and Yannick Moy.
Automating the verification of floating-point programs.
In Andrei Paskevich and Thomas Wies, editors, Verified Software:
Theories, Tools, and Experiments. Revised Selected Papers Presented at the
9th International Conference VSTTE, number 10712 in Lecture Notes in
Computer Science, Heidelberg, Germany, December 2017. Springer.
[ bib |
full text on HAL ]
|
|
[19]
|
Nicolas Jeannerod, Claude Marché, and Ralf Treinen.
A formally verified interpreter for a shell-like programming
language.
In Andrei Paskevich and Thomas Wies, editors, Verified Software:
Theories, Tools, and Experiments. Revised Selected Papers Presented at the
9th International Conference VSTTE, number 10712 in Lecture Notes in
Computer Science, Heidelberg, Germany, December 2017. Springer.
[ bib |
full text on HAL ]
|
|
[18]
|
Jean-Christophe Filliâtre.
Why3 --- where programs meet provers.
In KeY Symposium 2017, Rastatt, Germany, October 2017.
Invited talk.
[ bib ]
|
|
[17]
|
Sylvie Boldo, Mioara Joldes, Jean-Michel Muller, and Valentina Popescu.
Formal verification of a floating-point expansion renormalization
algorithm.
In Proceedings of the 8th International Conference on
Interactive Theorem Proving, Brasilia, Brazil, September 2017.
[ bib |
full text on HAL |
.pdf ]
|
|
[16]
|
Florian Faissole.
Formalization and closedness of finite dimensional subspaces.
In SYNASC 2017 - 19th International Symposium on Symbolic and
Numeric Algorithms for Scientific Computing, Timisoara, Romania, September
2017.
[ bib |
http |
.pdf ]
Keywords: filters ; finite dimensional subspaces ; formalization of mathematics ; functional analysis ; formal proof ; Coq
|
|
[15]
|
Sylvie Boldo, Florian Faissole, and Alexandre Chapoutot.
Round-off error analysis of explicit one-step numerical integration
methods.
In 24th IEEE Symposium on Computer Arithmetic, London, United
Kingdom, July 2017.
[ bib |
DOI |
full text on HAL |
.pdf ]
|
|
[14]
|
Ran Chen and Jean-Jacques Lévy.
A semi-automatic proof of strong connectivity.
In 9th Working Conference on Verified Software: Theories, Tools
and Experiments (VSTTE), Heidelberg, Germany, July 2017.
[ bib |
full text on HAL ]
|
|
[13]
|
Raphaël Rieu-Helft, Claude Marché, and Guillaume Melquiond.
How to get an efficient yet verified arbitrary-precision integer
library.
In 9th Working Conference on Verified Software: Theories, Tools,
and Experiments, volume 10712 of Lecture Notes in Computer Science,
pages 84--101, Heidelberg, Germany, July 2017.
[ bib |
DOI |
full text on HAL |
.pdf ]
Keywords: arbitrary-precision arithmetic ; deductive program verification ; C language ; Why3 program verifier
|
|
[12]
|
Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and
Micaela Mayero.
Preuve formelle du théorème de Lax--Milgram.
In 16èmes journées Approches Formelles dans
l'Assistance au Développement de Logiciels, Montpellier, France, June
2017.
[ bib |
full text on HAL |
.pdf ]
|
|
[11]
|
Jean-Christophe Filliâtre.
Why3 tutorial.
In VerifyThis 2017, Uppsala, Sweden, April 2017.
Invited tutorial.
[ bib ]
|
|
[10]
|
Nicolas Jeannerod.
Le coquillage dans le CoLiS-mateur: formalisation d'un langage de
programmation de type Shell.
In Sylvie Boldo and Julien Signoles, editors, Vingt-huitièmes
Journées Francophones des Langages Applicatifs, Gourette, France, January
2017.
[ bib ]
|
|
[9]
|
Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and
Micaela Mayero.
A Coq Formal Proof of the Lax-Milgram theorem.
In Proceedings of the 6th ACM SIGPLAN Conference on Certified
Programs and Proofs, CPP 2017, pages 79--89, New York, NY, USA, January
2017. ACM.
[ bib |
DOI |
full text on HAL |
.pdf ]
|
|
[8]
|
Ran Chen and Jean-Jacques Lévy.
Une preuve formelle de l'algorithme de Tarjan-1972 pour trouver les
composantes fortement connexes dans un graphe.
In Sylvie Boldo and Julien Signoles, editors, Vingt-huitièmes
Journées Francophones des Langages Applicatifs, Gourette, France, January
2017.
[ bib |
full text on HAL ]
|
|
[7]
|
Martin Clochard.
Preuves taillées en biseau.
In Sylvie Boldo and Julien Signoles, editors, Vingt-huitièmes
Journées Francophones des Langages Applicatifs, Gourette, France, January
2017.
[ bib |
full text on HAL ]
|
|
[6]
|
Mário Pereira.
Défonctionnaliser pour prouver.
In Sylvie Boldo and Julien Signoles, editors, Vingt-huitièmes
Journées Francophones des Langages Applicatifs, Gourette, France, January
2017.
[ bib |
full text on HAL ]
|
|
[5]
|
Sylvain Conchon, Mohamed Iguernlala, Kailiang Ji, Guillaume Melquiond, and
Clément Fumex.
A three-tier strategy for reasoning about floating-point numbers in
SMT.
In Computer Aided Verification, volume 10427 of Lecture
Notes in Computer Science, pages 419--435, 2017.
[ bib |
DOI |
full text on HAL ]
|
|
[4]
|
Raphaël Rieu-Helft and Pascal Cuoq.
Result graphs for an abstract interpretation-based static analyzer.
In Sylvie Boldo and Julien Signoles, editors, Vingt-huitièmes
Journées Francophones des Langages Applicatifs, Gourette, France, January
2017.
[ bib ]
|
|
[3]
|
Sylvain Conchon, David Declerck, and Fatiha Zaïdi.
Compiling parameterized x86-tso concurrent programs to cubicle-w.
In Zhenhua Duan and Luke Ong, editors, International Conference
on Formal Engineering Methods, number 10610 in Lecture Notes in Computer
Science, pages 88--104, 2017.
[ bib ]
|
|
[2]
|
Florian Faissole and Bas Spitters.
Synthetic topology in HoTT for probabilistic programming.
In The Third International Workshop on Coq for Programming
Languages (CoqPL 2017), Paris, France, January 2017.
[ bib |
full text on HAL ]
|
|
[1]
|
Sylvain Conchon, Amit Goel, Sava Krstic, Rupak Majumdar, and Mattias Roux.
FAR-Cubicle - A new reachability algorithm for Cubicle.
In Daryl Stewart and Georg Weissenbacher, editors, Formal
Methods in Computer Aided Design, pages 172--175, 2017.
[ bib |
DOI |
full text on HAL ]
|
|
[6]
|
Andrei Paskevich and Thomas Wies, editors.
Verified Software: Theories, Tools, and Experiments. Revised
Selected Papers Presented at the 9th International Conference VSTTE,
number 10712 in Lecture Notes in Computer Science, Heidelberg, Germany,
December 2017. Springer.
[ bib |
full text on HAL ]
|
|
[5]
|
Arthur Charguéraud, Jean-Christophe Filliâtre, Mário Pereira, and
François Pottier.
VOCAL -- A Verified OCaml Library.
ML Family Workshop, September 2017.
[ bib |
full text on HAL ]
|
|
[4]
|
Alessandro Abate and Sylvie Boldo, editors.
10th International Workshop on Numerical Software Verification.
Springer, July 2017.
[ bib |
full text on HAL ]
|
|
[3]
|
Jean-Christophe Filliâtre.
Vérification déductive de programmes.
Séminaire Acquérir une culture commune dans le domaine de
l'informatique, lycée Diderot, Paris, May 2017.
Séminaire invité.
[ bib ]
|
|
[2]
|
Florian Faissole and Bas Spitters.
Synthetic topology in homotopy type theory for probabilistic
programming.
PPS 2017 - Workshop on probabilistic programming semantics, January
2017.
Poster.
[ bib |
full text on HAL ]
|
|
[1]
|
Sylvie Boldo and Julien Signoles, editors.
Journées Francophones des Langages Applicatifs, Gourette,
France, January 2017.
[ bib |
full text on HAL ]
|