[20]

Clément Fumex, Claude Marché, and Yannick Moy.
Automating the verification of floatingpoint 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 shelllike 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]

JeanChristophe Filliâtre.
Why3  where programs meet provers.
In KeY Symposium 2017, Rastatt, Germany, October 2017.
Invited talk.
[ bib ]

[17]

Sylvie Boldo, Mioara Joldes, JeanMichel Muller, and Valentina Popescu.
Formal verification of a floatingpoint 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.
Roundoff error analysis of explicit onestep 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 JeanJacques Lévy.
A semiautomatic 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 RieuHelft, Claude Marché, and Guillaume Melquiond.
How to get an efficient yet verified arbitraryprecision integer
library.
In 9th Working Conference on Verified Software: Theories, Tools,
and Experiments, volume 10712 of Lecture Notes in Computer Science,
pages 84101, Heidelberg, Germany, July 2017.
[ bib 
DOI 
full text on HAL 
.pdf ]
Keywords: arbitraryprecision 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 LaxMilgram.
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]

JeanChristophe Filliâtre.
Why3 tutorial.
In VerifyThis 2017, Uppsala, Sweden, April 2017.
Invited tutorial.
[ bib ]

[10]

Nicolas Jeannerod.
Le coquillage dans le CoLiSmateur: formalisation d'un langage de
programmation de type Shell.
In Sylvie Boldo and Julien Signoles, editors, Vingthuitiè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 LaxMilgram theorem.
In Proceedings of the 6th ACM SIGPLAN Conference on Certified
Programs and Proofs, CPP 2017, pages 7989, New York, NY, USA, January
2017. ACM.
[ bib 
DOI 
full text on HAL 
.pdf ]

[8]

Ran Chen and JeanJacques Lévy.
Une preuve formelle de l'algorithme de Tarjan1972 pour trouver les
composantes fortement connexes dans un graphe.
In Sylvie Boldo and Julien Signoles, editors, Vingthuitiè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, Vingthuitiè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, Vingthuitiè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 threetier strategy for reasoning about floatingpoint numbers in
SMT.
In Computer Aided Verification, volume 10427 of Lecture
Notes in Computer Science, pages 419435, 2017.
[ bib 
DOI 
full text on HAL ]

[4]

Raphaël RieuHelft and Pascal Cuoq.
Result graphs for an abstract interpretationbased static analyzer.
In Sylvie Boldo and Julien Signoles, editors, Vingthuitièmes
Journées Francophones des Langages Applicatifs, Gourette, France, January
2017.
[ bib ]

[3]

Sylvain Conchon, David Declerck, and Fatiha Zaïdi.
Compiling parameterized x86tso concurrent programs to cubiclew.
In Zhenhua Duan and Luke Ong, editors, International Conference
on Formal Engineering Methods, number 10610 in Lecture Notes in Computer
Science, pages 88104, 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.
FARCubicle  A new reachability algorithm for Cubicle.
In Daryl Stewart and Georg Weissenbacher, editors, Formal
Methods in Computer Aided Design, pages 172175, 2017.
[ bib 
DOI 
full text on HAL ]
