EN FR
EN FR


previous Previous | up Home


Bibliography

Major publications by the team in recent years
  • 1F. Bobot, J.-C. Filliâtre, C. Marché, A. Paskevich.

    Let's Verify This with Why3, in: International Journal on Software Tools for Technology Transfer (STTT), 2015, vol. 17, no 6, pp. 709–727.

    http://hal.inria.fr/hal-00967132/en
  • 2S. Boldo, J.-H. Jourdan, X. Leroy, G. Melquiond.

    Verified Compilation of Floating-Point Computations, in: Journal of Automated Reasoning, February 2015, vol. 54, no 2, pp. 135-163.

    https://hal.inria.fr/hal-00862689
  • 3S. Boldo, G. Melquiond.

    Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the Coq System, ISTE Press - Elsevier, December 2017.

    https://hal.inria.fr/hal-01632617
  • 4M. Clochard, L. Gondelman, M. Pereira.

    The Matrix Reproved, in: Journal of Automated Reasoning, 2018, vol. 60, no 3, pp. 365–383.

    https://hal.inria.fr/hal-01617437
  • 5S. Conchon, M. Iguernlala, K. Ji, G. Melquiond, C. Fumex.

    A Three-tier Strategy for Reasoning about Floating-Point Numbers in SMT, in: Computer Aided Verification, 2017.

    https://hal.inria.fr/hal-01522770
  • 6J.-C. Filliâtre, L. Gondelman, A. Paskevich.

    The Spirit of Ghost Code, in: Formal Methods in System Design, 2016, vol. 48, no 3, pp. 152–174.

    https://hal.archives-ouvertes.fr/hal-01396864v1
  • 7C. Fumex, C. Dross, J. Gerlach, C. Marché.

    Specification and Proof of High-Level Functional Properties of Bit-Level Programs, in: 8th NASA Formal Methods Symposium, Minneapolis, MN, USA, S. Rayadurgam, O. Tkachuk (editors), Lecture Notes in Computer Science, Springer, June 2016, vol. 9690, pp. 291–306.

    https://hal.inria.fr/hal-01314876
  • 8É. Martin-Dorel, G. Melquiond.

    Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq, in: Journal of Automated Reasoning, 2016.

    https://hal.inria.fr/hal-01086460
  • 9G. Melquiond, R. Rieu-Helft.

    A Why3 Framework for Reflection Proofs and its Application to GMP's Algorithms, in: 9th International Joint Conference on Automated Reasoning, Oxford, United Kingdom, D. Galmiche, S. Schulz, R. Sebastiani (editors), Lecture Notes in Computer Science, July 2018.

    https://hal.inria.fr/hal-01699754
  • 10P. Roux, M. Iguernlala, S. 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.

    https://hal.archives-ouvertes.fr/hal-01737737
Publications of the year

Doctoral Dissertations and Habilitation Theses

Articles in International Peer-Reviewed Journals

  • 12S. Boldo, F. Faissole, A. Chapoutot.

    Round-off error and exceptional behavior analysis of explicit Runge-Kutta methods, in: IEEE Transactions on Computers, 2019, forthcoming. [ DOI : 10.1109/TC.2019.2917902 ]

    https://hal.archives-ouvertes.fr/hal-01883843
  • 13D. Gallois-Wong, S. Boldo, P. Cuoq.

    Optimal Inverse Projection of Floating-Point Addition, in: Numerical Algorithms, 2019, forthcoming. [ DOI : 10.1007/s11075-019-00711-z ]

    https://hal.inria.fr/hal-01939097
  • 14A. Mahboubi, G. Melquiond, T. Sibut-Pinote.

    Formally Verified Approximations of Definite Integrals, in: Journal of Automated Reasoning, February 2019, vol. 62, no 2, pp. 281-300. [ DOI : 10.1007/s10817-018-9463-7 ]

    https://hal.inria.fr/hal-01630143
  • 15E. Neumann, F. Steinberg.

    Parametrised second-order complexity theory with applications to the study of interval computation, in: Theoretical Computer Science, 2019, forthcoming. [ DOI : 10.1016/j.tcs.2019.05.009 ]

    https://hal.inria.fr/hal-02148494
  • 16A. Volkova, T. Hilaire, C. Lauter.

    Arithmetic approaches for rigorous design of reliable Fixed-Point LTI filters, in: IEEE Transactions on Computers, 2019, pp. 1-14, forthcoming. [ DOI : 10.1109/TC.2019.2950658 ]

    https://hal.archives-ouvertes.fr/hal-01918650

Invited Conferences

  • 17J.-C. Filliâtre.

    Deductive Verification of OCaml Libraries, in: iFM 2019 - International Conference on integrated Formal Methods, Bergen, Norway, December 2019.

    https://hal.inria.fr/hal-02406253
  • 18J.-C. Filliâtre.

    Retour sur 25 ans de programmation avec OCaml, in: JFLA 2019 - Journées Francophones des Langages Applicatifs, Les Rousses, France, January 2019.

    https://hal.inria.fr/hal-02406208
  • 19G. Melquiond.

    Computer Arithmetic and Formal Proofs, in: 30èmes Journées Francophones des Langages Applicatifs, Les Rousses, France, N. Magaud (editor), January 2019.

    https://hal.inria.fr/hal-02013540

International Conferences with Proceedings

  • 20B. Becker, C. Marché.

    Ghost Code in Action: Automated Verification of a Symbolic Interpreter, in: VSTTE 2019 - 11th Working Conference on Verified Software: Tools, Techniques and Experiments, New York, United States, S. Chakraborty, J. A.Navas (editors), Lecture Notes in Computer Science, September 2019.

    https://hal.inria.fr/hal-02276257
  • 21C. Belo Lourenço, M. J. Frade, J. Sousa Pinto.

    A Generalized Program Verification Workflow Based on Loop Elimination and SA Form, in: FormaliSE 2019 - 7th International Conference on Formal Methods in Software Engineering, Montreal, Canada, May 2019.

    https://hal.inria.fr/hal-02431769
  • 22V. Blot, A. Bousalem, Q. Garchery, C. Keller.

    SMTCoq: automatisation expressive et extensible dans Coq, in: Journées Francophones des Langages Applicatifs, Les Rousses, France, January 2019.

    https://hal.archives-ouvertes.fr/hal-02369249
  • 23A. Charguéraud, J.-C. Filliâtre, C. Lourenço, M. Pereira.

    GOSPEL -Providing OCaml with a Formal Specification Language, in: FM 2019 - 23rd International Symposium on Formal Methods, Porto, Portugal, October 2019.

    https://hal.inria.fr/hal-02157484
  • 24M. Clochard, C. Marché, A. Paskevich.

    Deductive Verification with Ghost Monitors, in: Principles of Programming Languages, New Orleans, United States, 2020. [ DOI : 10.1145/3371070 ]

    https://hal.inria.fr/hal-02368284
  • 25S. Conchon, M. Roux.

    Reasoning about Universal Cubes in MCMT, in: Formal Methods and Software Engineering, Shenzhen, China, Lecture Notes in Computer Science, 2019, no 11852, pp. 270–285.

    https://hal.archives-ouvertes.fr/hal-02420588
  • 26T. Hilaire, H. Ouzia, B. Lopez.

    Optimal Word-Length Allocation for the Fixed-Point Implementation of Linear Filters and Controllers, in: 2019 IEEE 26th Symposium on Computer Arithmetic (ARITH), Kyoto, Japan, IEEE, June 2019, pp. 175-182. [ DOI : 10.1109/ARITH.2019.00040 ]

    https://hal.sorbonne-universite.fr/hal-02393851
  • 27A. Kawamura, F. Steinberg, H. Thies.

    Second-Order Linear-Time Computability with Applications to Computable Analysis, in: TAMC 2019 - 15th Annual Conference Theory and Applications of Models of Computation, Tokyo, Japan, T. V. Gopal, J. Watada (editors), LNCS - Lecture Notes in Computer Science, Springer, March 2019, vol. 11436, pp. 337-358.

    https://hal.inria.fr/hal-02148490
  • 28G. Melquiond, R. Rieu-Helft.

    Formal Verification of a State-of-the-Art Integer Square Root, in: ARITH-26 2019 - 26th IEEE 26th Symposium on Computer Arithmetic, Kyoto, Japan, S. Boldo, M. Langhammer (editors), June 2019, pp. 183-186. [ DOI : 10.1109/ARITH.2019.00041 ]

    https://hal.inria.fr/hal-02092970
  • 29F. Steinberg, H. Thies, L. Théry.

    Quantitative continuity and Computable Analysis in Coq, in: ITP 2019 - Tenth International Conference on Interactive Theorem Proving, Portland, United States, 2019, The version accepted to the conference can be accessed at https://drops.dagstuhl.de/opus/volltexte/2019/11083/. [ DOI : 10.4230/LIPIcs.ITP.2019.28 ]

    https://hal.archives-ouvertes.fr/hal-02426470

National Conferences with Proceedings

  • 30J.-C. Filliâtre.

    Mesurer la hauteur d'un arbre, in: Journées Francophones des Langages Applicatifs, Gruissan, France, January 2020.

    https://hal.inria.fr/hal-02315541
  • 31D. Gallois-Wong.

    Formalisation en Coq d'algorithmes de filtres numériques, in: Journées Francophones des Langages Applicatifs (JFLA) 2019, Les Rousses, France, Journées Francophones des Langages Applicatifs 2019, Nicolas Magaud, January 2019.

    https://hal.inria.fr/hal-01929531
  • 32Q. Garchery, C. Keller, C. Marché, A. Paskevich.

    Des transformations logiques passent leur certicat, in: Journées Francophones des Langages Applicatifs, Gruissan, France, 2020.

    https://hal.inria.fr/hal-02384946
  • 33R. Rieu-Helft.

    Un mécanisme de preuve par réflexion pour Why3 et son application aux algorithmes de GMP, in: JFLA 2019 - 30èmes Journées Francophones des Langages Applicatifs, Rousses, France, January 2019.

    https://hal.inria.fr/hal-01943010

Conferences without Proceedings

  • 34F. Faissole.

    Formalisation en Coq des erreurs d'arrondi de méthodes de Runge-Kutta pour les systèmes matriciels, in: AFADL 2019 - 18e journées Approches Formelles dans l'Assistance au Développement de Logiciels, Toulouse, France, June 2019.

    https://hal.archives-ouvertes.fr/hal-02391924

Scientific Books (or Scientific Book chapters)

  • 35Proceedings of the 26th Symposium on Computer Arithmetic (ARITH 2019), IEEE, Kyoto, June 2019. [ DOI : 10.1109/ARITH.2019.00005 ]

    https://hal.inria.fr/hal-02433652
  • 36T. Balabonski, S. Conchon, J.-C. Filliâtre, K. Nguyễn.

    Numérique et Sciences Informatiques, 30 leçons avec exercices corrigés, Ellipses, August 2019.

    https://hal.inria.fr/hal-02379073

Internal Reports

  • 37L. Andrès.

    Vérification par preuve formelle de propriétés fonctionnelles d'algorithme de classification, Université Paris Sud (Paris 11) - Université Paris Saclay, August 2019.

    https://hal.inria.fr/hal-02421484
  • 38B. Becker, N. Jeannerod, C. Marché, R. Treinen.

    Revision 2 of CoLiS language: formal syntax, semantics, concrete and symbolic interpreters, ANR, October 2019.

    https://hal.inria.fr/hal-02321743
  • 39M. Huisman, R. Monahan, P. Müller, A. Paskevich, G. Ernst.

    VerifyThis 2018: A Program Verification Competition, Université Paris-Saclay, January 2019.

    https://hal.inria.fr/hal-01981937
  • 40N. Jeannerod, C. Marché, Y. Régis-Gianas, M. Sighireanu, R. Treinen.

    Specification of UNIX Utilities, ANR, October 2019.

    https://hal.inria.fr/hal-02321691

Other Publications

  • 41B. Becker, N. Jeannerod, C. Marché, Y. Régis-Gianas, M. Sighireanu, R. Treinen.

    Analysing installation scenarios of Debian packages, 2019, working paper or preprint.

    https://hal.archives-ouvertes.fr/hal-02355602
  • 42S. Boldo, C. Q. Lauter, J.-M. Muller.

    Emulating round-to-nearest-ties-to-zero "augmented" floating-point operations using round-to-nearest-ties-to-even arithmetic, October 2019, working paper or preprint.

    https://hal.archives-ouvertes.fr/hal-02137968
  • 43M. Clochard.

    Méthodes et outils pour la spécification et la preuve de propriétés difficiles de programmes séquentiels (Documents de soutenance), February 2019.

    https://hal.inria.fr/hal-02047458
  • 44F. Faissole, G. Constantinides, D. Thomas.

    Formalizing loop-carried dependencies in Coq for high-level synthesis, April 2019, FCCM 2019 - 27th IEEE Symposium on Field-Programmable Custom Computing Machines, Poster.

    https://hal.archives-ouvertes.fr/hal-02391954
  • 45F. Steinberg, H. Thies.

    Some formal proofs of isomorphy and discontinuity, March 2019, MLA 2019 - Third Workshop on Mathematical Logic and its Applications.

    https://hal.inria.fr/hal-02019174
  • 46F. Steinberg, L. Théry, H. Thies.

    Quantitative continuity and computable analysis in Coq, April 2019, working paper or preprint.

    https://hal.inria.fr/hal-02088293
References in notes
  • 47A. Ayad, C. Marché.

    Multi-Prover Verification of Floating-Point Programs, in: Fifth International Joint Conference on Automated Reasoning, Edinburgh, Scotland, J. Giesl, R. Hähnle (editors), Lecture Notes in Artificial Intelligence, Springer, July 2010, vol. 6173, pp. 127–141.

    http://hal.inria.fr/inria-00534333
  • 48C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanović, T. King, A. Reynolds, C. Tinelli.

    CVC4, in: Proceedings of the 23rd international conference on Computer aided verification, Berlin, Heidelberg, CAV'11, Springer-Verlag, 2011, pp. 171–177.
  • 49P. Baudin, J.-C. Filliâtre, C. Marché, B. Monate, Y. Moy, V. Prevosto.

    ACSL: ANSI/ISO C Specification Language, version 1.4, 2009.
  • 50P. Behm, P. Benoit, A. Faivre, J.-M. Meynadier.

    METEOR : A successful application of B in a large project, in: Proceedings of FM'99: World Congress on Formal Methods, J. M. Wing, J. Woodcock, J. Davies (editors), Lecture Notes in Computer Science (Springer-Verlag), Springer Verlag, September 1999, pp. 369–387.
  • 51S. Boldo, F. Clément, J.-C. Filliâtre, M. Mayero, G. Melquiond, P. Weis.

    Formal Proof of a Wave Equation Resolution Scheme: the Method Error, in: Proceedings of the First Interactive Theorem Proving Conference, Edinburgh, Scotland, M. Kaufmann, L. C. Paulson (editors), LNCS, Springer, July 2010, vol. 6172, pp. 147–162.

    http://hal.inria.fr/inria-00450789/
  • 52S. Boldo, F. Clément, J.-C. Filliâtre, M. Mayero, G. Melquiond, P. Weis.

    Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program, in: Journal of Automated Reasoning, April 2013, vol. 50, no 4, pp. 423–456.

    http://hal.inria.fr/hal-00649240/en/
  • 53S. Boldo, J.-C. Filliâtre, G. Melquiond.

    Combining Coq and Gappa for Certifying Floating-Point Programs, in: 16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Grand Bend, Canada, Lecture Notes in Artificial Intelligence, Springer, July 2009, vol. 5625, pp. 59–74.
  • 54S. Boldo, C. Marché.

    Formal verification of numerical programs: from C annotated programs to mechanical proofs, in: Mathematics in Computer Science, 2011, vol. 5, pp. 377–393.

    http://hal.inria.fr/hal-00777605
  • 55S. Boldo, T. M. T. Nguyen.

    Proofs of numerical programs when the compiler optimizes, in: Innovations in Systems and Software Engineering, 2011, vol. 7, pp. 151–160.

    http://hal.inria.fr/hal-00777639
  • 56L. Burdy, Y. Cheon, D. R. Cok, M. D. Ernst, J. R. Kiniry, G. T. Leavens, K. R. M. Leino, E. Poll.

    An overview of JML tools and applications, in: International Journal on Software Tools for Technology Transfer (STTT), June 2005, vol. 7, no 3, pp. 212–232.
  • 57M. Clochard.

    Méthodes et outils pour la spécification et la preuve de propriétés difficiles de programmes séquentiels, Université Paris-Saclay, March 2018.

    https://tel.archives-ouvertes.fr/tel-01787689
  • 58S. Conchon, A. Coquereau, M. Iguernlala, A. Mebsout.

    Alt-Ergo 2.2, in: SMT Workshop: International Workshop on Satisfiability Modulo Theories, Oxford, United Kingdom, July 2018.

    https://hal.inria.fr/hal-01960203
  • 59C. Fumex, C. Marché, Y. Moy.

    Automating the Verification of Floating-Point Programs, in: Verified Software: Theories, Tools, and Experiments. Revised Selected Papers Presented at the 9th International Conference VSTTE, Heidelberg, Germany, A. Paskevich, T. Wies (editors), Lecture Notes in Computer Science, Springer, December 2017, no 10712.

    https://hal.inria.fr/hal-01534533/
  • 60N. Jeannerod, C. Marché, R. Treinen.

    A Formally Verified Interpreter for a Shell-like Programming Language, in: Verified Software: Theories, Tools, and Experiments. Revised Selected Papers Presented at the 9th International Conference VSTTE, Heidelberg, Germany, A. Paskevich, T. Wies (editors), Lecture Notes in Computer Science, Springer, December 2017, no 10712.

    https://hal.inria.fr/hal-01534747v1
  • 61N. Jeannerod, R. Treinen.

    Deciding the First-Order Theory of an Algebra of Feature Trees with Updates, in: 9th International Joint Conference on Automated Reasoning, Oxford, United Kingdom, July 2018.

    https://hal.archives-ouvertes.fr/hal-01807474
  • 62G. Klein, J. Andronick, K. Elphinstone, G. Heiser, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, S. Winwood.

    seL4: Formal verification of an OS kernel, in: Communications of the ACM, June 2010, vol. 53, no 6, pp. 107–115.
  • 63X. Leroy.

    A formally verified compiler back-end, in: Journal of Automated Reasoning, 2009, vol. 43, no 4, pp. 363–446.

    http://hal.inria.fr/inria-00360768/en/
  • 64A. Mahboubi, G. Melquiond, T. Sibut-Pinote.

    Formally Verified Approximations of Definite Integrals, in: Proceedings of the 7th International Conference on Interactive Theorem Proving, Nancy, France, J. C. Blanchette, S. Merz (editors), Lecture Notes in Computer Science, August 2016, vol. 9807.

    https://hal.inria.fr/hal-01289616
  • 65J.-M. Muller, N. Brunie, F. de Dinechin, C.-P. Jeannerod, M. Joldes, V. Lefèvre, G. Melquiond, N. Revol, S. Torres.

    Handbook of Floating-point Arithmetic (2nd edition), Birkhäuser Basel, July 2018.

    https://hal.inria.fr/hal-01766584
  • 66T. M. T. Nguyen, C. Marché.

    Hardware-Dependent Proofs of Numerical Programs, in: Certified Programs and Proofs, J.-P. Jouannaud, Z. Shao (editors), Lecture Notes in Computer Science, Springer, December 2011, pp. 314–329.

    http://hal.inria.fr/hal-00772508
  • 67R. Rieu-Helft.

    Un mécanisme d'extraction vers C pour Why3, in: Vingt-neuvièmes Journées Francophones des Langages Applicatifs, Banyuls-sur-mer, France, S. Boldo, N. Magaud (editors), January 2018.

    https://hal.inria.fr/hal-01653153
  • 68F. de Dinechin, C. Lauter, G. Melquiond.

    Certifying the floating-point implementation of an elementary function using Gappa, in: IEEE Transactions on Computers, 2011, vol. 60, no 2, pp. 242–253.

    http://hal.inria.fr/inria-00533968/en/
  • 69S. de Gouw, J. Rot, F. S. de Boer, R. Bubel, R. Hähnle.

    , OpenJDK's Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst CaseD. Kroening, C. S. Păsăreanu (editors), Springer International Publishing, Cham, 2015, pp. 273–289.
  • 70L. de Moura, N. Bjørner.

    Z3, An Efficient SMT Solver, in: TACAS, Lecture Notes in Computer Science, Springer, 2008, vol. 4963, pp. 337–340.


previous Previous | up Home