Wiki Agenda Contact Version française

Publications 2018

Back

Books / Journals / Conferences / PhD theses / Misc. / Reports

Books and book chapters

[1] Jean-Michel Muller, Nicolas Brunie, Florent de Dinechin, Claude-Pierre Jeannerod, Mioara Joldes, Vincent Lefèvre, Guillaume Melquiond, Nathalie Revol, and Serge Torres. Handbook of Floating-point Arithmetic (2nd edition). Birkhäuser Basel, July 2018. [ bib | DOI | full text on HAL ]
Keywords: arithmetic operators ; arithmetic algorithms ; numerical computing ; floating-point arithmetic ; computer arithmetic

Journals

[4] Assia Mahboubi, Guillaume Melquiond, and Thomas Sibut-Pinote. Formally verified approximations of definite integrals. Journal of Automated Reasoning, March 2018. [ bib | full text on HAL ]
[3] Martin Clochard, Léon Gondelman, and Mário Pereira. The Matrix reproved. Journal of Automated Reasoning, 60(3):365--383, 2018. [ bib | DOI | full text on HAL ]
[2] Sylvain Dailler, David Hauzar, Claude Marché, and Yannick Moy. Instrumenting a weakest precondition calculus for counterexample generation. Journal of Logical and Algebraic Methods in Programming, 99:97--113, 2018. [ bib | full text on HAL ]
Keywords: Deductive Program Verification ; Weakest Precondition Calculus ; Satisfiability Modulo Theories ; Counterexamples
[1] Anastasia Volkova, Matei Istoan, Florent de Dinechin, and Thibault Hilaire. Towards hardware IIR filters computing just right: Direct form I case study. IEEE Transactions on Computers, 2018. [ bib | full text on HAL ]
Keywords: computer arithmetic ; fixed-point ; FPGA ; error analysis ; digital filters ; constant multiplication

Conferences

[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 | 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 ]

PhD theses

[3] Mário Pereira. Tools and Techniques for the Verification of Modular Stateful Code. Thèse de doctorat, Université Paris-Saclay, December 2018. [ bib ]
[2] David Declerck. Verification via Model Checking of Parameterized Concurrent Programs on Weak Memory Models. Thèse de doctorat, Université Paris-Saclay, September 2018. [ bib | full text on HAL ]
Keywords: Weak memory ; Model checking ; Verification ; Mémoire faible
[1] Martin Clochard. Méthodes et outils pour la spécification et la preuve de propriétés difficiles de programmes séquentiels. Thèse de doctorat, Université Paris-Saclay, March 2018. [ bib | full text on HAL ]

Misc.

[6] Martin Clochard, Claude Marché, and Andrei Paskevich. Deductive verification with ghost monitors. Working paper, November 2018. [ bib | full text on HAL ]
Keywords: deductive verification ; unstructured programs ; ghost code ; games ; Hoare logic ; predicate transformers ; infinite behaviors
[5] 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 ]
[4] 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
[3] Jean-Christophe Filliâtre. Parcours d'un informaticien. Séminaire Info Pour Tous, September 2018. Séminaire invité. [ bib | http ]
[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 ]

Reports

[1] Martin Clochard, Andrei Paskevich, and Claude Marché. Deductive verification via ghost debugging. Research Report 9219, Inria, 2018. [ bib | full text on HAL ]

Back

Books / Journals / Conferences / PhD theses / Misc. / Reports


This page was generated by bibtex2html.