|
[13]
|
Guillaume Melquiond and Raphaël Rieu-Helft.
A Why3 framework for reflection proofs and its application to
GMP's algorithms.
In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors,
9th International Joint Conference on Automated Reasoning, Lecture
Notes in Computer Science, Oxford, United Kingdom, July 2018.
[ bib |
full text on HAL ]
|
|
[12]
|
Jean-Christophe Filliâtre.
Auto-active verification using Why3's IDE.
In 4th Workshop on Formal Integrated Development Environment,
Oxford, UK, July 2018.
Invited talk.
[ bib ]
|
|
[11]
|
Sylvain Conchon, Albin Coquereau, Mohamed Iguernlala, and Alain Mebsout.
Alt-Ergo 2.2.
In SMT Workshop: International Workshop on Satisfiability Modulo
Theories, Oxford, United Kingdom, July 2018.
[ bib |
full text on HAL |
.pdf ]
|
|
[10]
|
Sylvie Boldo, Florian Faissole, and Vincent Tourneur.
A formally-proved algorithm to compute the correct average of decimal
floating-point numbers.
In 25th IEEE Symposium on Computer Arithmetic, Amherst, MA,
United States, June 2018.
[ bib |
full text on HAL ]
|
|
[9]
|
Pierre Roux, Mohamed Iguernlala, and Sylvain Conchon.
A non-linear arithmetic procedure for control-command software
verification.
In 24th International Conference on Tools and Algorithms for the
Construction and Analysis of Systems (TACAS), Thessalonique, Greece, April
2018.
[ bib |
full text on HAL ]
|
|
[8]
|
Florian Faissole and Bas Spitters.
Preuves constructives de programmes probabilistes.
In Sylvie Boldo and Nicolas Magaud, editors, Vingt-neuvièmes
Journées Francophones des Langages Applicatifs, Banyuls-sur-mer, France,
January 2018.
[ bib |
full text on HAL ]
|
|
[7]
|
Florian Faissole.
Définir le fini : deux formalisations d'espaces de dimension
finie.
In Sylvie Boldo and Nicolas Magaud, editors, Vingt-neuvièmes
Journées Francophones des Langages Applicatifs, Banyuls-sur-mer, France,
January 2018.
[ bib |
full text on HAL |
.pdf ]
|
|
[6]
|
Raphaël Rieu-Helft.
Un mécanisme d'extraction vers C pour Why3.
In Sylvie Boldo and Nicolas Magaud, editors, Vingt-neuvièmes
Journées Francophones des Langages Applicatifs, Banyuls-sur-mer, France,
January 2018.
[ bib |
full text on HAL |
.pdf ]
|
|
[5]
|
Jean-Christophe Filliâtre, Mário Pereira, and Simão Melo de Sousa.
Vérification de programmes fortement impératifs avec Why3.
In Sylvie Boldo and Nicolas Magaud, editors, Vingt-neuvièmes
Journées Francophones des Langages Applicatifs, Banyuls-sur-mer, France,
January 2018.
[ bib |
full text on HAL |
.pdf ]
|
|
[4]
|
Sylvain Dailler, Claude Marché, and Yannick Moy.
Lightweight interactive proving inside an automatic program verifier.
In Proceedings of the Fourth Workshop on Formal Integrated
Development Environment, F-IDE, Oxford, UK, July 14, 2018, 2018.
[ bib |
DOI |
full text on HAL ]
|
|
[3]
|
Jean-Christophe Filliâtre.
Deductive program verification.
In Jeremy Avigad and Assia Mahboubi, editors, Interactive
Theorem Proving - 9th International Conference, ITP 2018, Held as Part of
the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018,
Proceedings, volume 10895 of Lecture Notes in Computer Science.
Springer, 2018.
Invited talk.
[ bib ]
|
|
[2]
|
Sylvain Conchon, David Declerck, and Fatiha Zaïdi.
Cubicle-w : Parameterized model checking on weak memory.
In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors,
International Joint Conference on Automated Reasoning, volume 10900 of
Lecture Notes in Computer Science, pages 152--160. Springer, 2018.
[ bib |
full text on HAL ]
|
|
[1]
|
Sylvain Conchon, Giorgio Delzanno, and Angelo Ferrando.
Declarative parameterized verification of topology-sensitive
distributed protocols.
In Andreas Podelski and François Taïani, editors,
Networked Systems, 6th International Conference, Revised Selected Papers,
Lecture Notes in Computer Science, pages 209--224, 2018.
[ bib |
full text on HAL ]
|
|
[6]
|
Georges-Axel Jaloyan, Claire Dross, Maroua Maalej, Yannick Moy, and Andrei
Paskevich.
Verification of programs with pointers in SPARK.
working paper https://hal.inria.fr/hal-01936105, November 2018.
[ bib |
full text on HAL ]
|
|
[5]
|
Anastasia Volkova, Thibault Hilaire, and Christoph Lauter.
Arithmetic approaches for rigorous design of reliable fixed-point
LTI filters.
working paper or preprint, November 2018.
[ bib |
full text on HAL ]
Keywords: Eigendecomposition ; Gershgorin circles ; Reliable Computations ; Floating-Point Arithmetic ; Digital Filters ; Interval Arithmetic ; Multiple Precision ; Fixed-Point Arithmetic ; Table Maker's Dilemma
|
|
[4]
|
Jean-Christophe Filliâtre.
Parcours d'un informaticien.
Séminaire Info Pour Tous, September 2018.
Séminaire invité.
[ bib |
http ]
|
|
[3]
|
Diane Gallois-Wong, Sylvie Boldo, and Thibault Hilaire.
A Coq formalization of digital filters.
August 2018.
[ bib |
DOI |
full text on HAL |
.pdf ]
|
|
[2]
|
Jean-Christophe Filliâtre.
An introduction to deductive program verification.
Mathematical Summer in Paris (summer school), July 2018.
Cours invité.
[ bib ]
|
|
[1]
|
Sylvie Boldo and Nicolas Magaud, editors.
Vingt-neuvièmes Journées Francophones des Langages
Applicatifs, Banyuls-sur-mer, France, January 2018.
[ bib |
full text on HAL ]
|