Wiki Agenda Contact Version française

Publications 2021

Back

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

Books and book chapters

Journals

[4] Jean-Christophe Filliâtre. Simpler proofs with decentralized invariants. Journal of Logical and Algebraic Methods in Programming, 121, January 2021. See https://usr.lmf.cnrs.fr/~jcf/spdi/. [ bib | DOI | full text on HAL ]
[3] Sylvie Boldo, Christoph Q. Lauter, and Jean-Michel Muller. Emulating round-to-nearest ties-to-zero ”augmented” floating-point operations using round-to-nearest ties-to-even arithmetic. IEEE Transactions on Computers, 70(7):1046--1058, 2021. [ bib | DOI | full text on HAL ]
[2] Florian Steinberg, Laurent Théry, and Holger Thies. Computable analysis and notions of continuity in Coq. Logical Methods in Computer Science, 2021. [ bib | DOI | full text on HAL ]
[1] Sylvain Conchon, Giorgio Delzanno, and Angelo Ferrando. Declarative parameterized verification of distributed protocols via the cubicle model checker. Fundam. Informaticae, 178(4):347--378, 2021. [ bib | DOI ]

Conferences

[13] Quentin Garchery. A framework for proof-carrying logical transformations. In Proof eXchange for Theorem Proving, volume 336 of Electronic Proceedings in Theoretical Computer Science, pages 5--23, July 2021. [ bib | DOI | full text on HAL ]
[12] Benedikt Becker, Cláudio Belo Lourenço, and Claude Marché. Explaining counterexamples with giant-step assertion checking. In José Creissac Campos and Andrei Paskevich, editors, 6th Workshop on Formal Integrated Development Environments (F-IDE 2021), Electronic Proceedings in Theoretical Computer Science, May 2021. [ bib | DOI | full text on HAL ]
[11] Jean-Christophe Filliâtre and Clément Pascutto. Ortac: Runtime assertion checking for OCaml. In Proceedings of the 21st International Conference on Runtime Verification (RV'21), May 2021. [ bib | full text on HAL ]
Runtime assertion checking (RAC) is a convenient set of techniques that lets developers abstract away the process of verifying the correctness of their programs by writing formal specifications and automating their verification at runtime. In this work, we present ortac, a runtime assertion checking tool for OCaml libraries and programs. OCaml is a functional programming lan- guage in which idioms rely on an expressive type system, modules, and interface abstractions. ortac consumes interfaces annotated with type invariants and function contracts and produces code wrappers with the same signature that check these specifications at runtime. It provides a flexible framework for traditional assertion checking, monitoring mis- behaviors without interruptions, and automated fuzz testing for OCaml programs. This paper presents an overview of ortac features and highlights its main design choices.

[10] Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, and Hiroaki Inoue. Automated verification of temporal properties of Ladder programs. In Formal Methods for Industrial Critical Systems, volume 12863 of Lecture Notes in Computer Science, pages 21--38, 2021. [ bib | DOI | full text on HAL ]
[9] Nicolas Osborne and Clément Pascutto. Leveraging formal specifications to generate fuzzing suites. In OCaml Users and Developers Workshop, co-located with the 26th ACM SIGPLAN International Conference on Functional Programming, 2021. [ bib | full text on HAL ]
[8] Jean-Christophe Filliâtre and Clément Pascutto. Ortac: Runtime assertion checking for OCaml. In 21st International Conference on Runtime Verification, 2021. [ bib | full text on HAL ]
[7] William Weens, Thibaud Vazquez-Gonzalez, and Louise Ben Salem-Knapp. Modeling round-off errors in hydrodynamic simulations. In 14th International Workshop on Numerical Software Verification, 2021. [ bib | full text on HAL ]
[6] Thibaut Balabonski, Antoine Lanco, and Guillaume Melquiond. A strong call-by-need calculus. In Naoki Kobayashi, editor, 6th International Conference on Formal Structures for Computation and Deduction, volume 195, pages 9:1--9:22, 2021. [ bib | DOI | full text on HAL ]
[5] Sylvie Boldo and Guillaume Melquiond. Some formal tools for computer arithmetic: Flocq and Gappa. In Mioara Joldes and Fabrizio Lamberti, editors, 28th IEEE International Symposium on Computer Arithmetic, 2021. [ bib | full text on HAL ]
[4] Louise Ben Salem-Knapp, Thibaud Vazquez-Gonzalez, and William Weens. La double précision suffit-elle à l'exascale ? In 20èmes journées Approches Formelles dans l'Assistance au Développement de Logiciels, 2021. [ bib | full text on HAL ]
[3] Guillaume Melquiond. Plotting in a formally verified way. In 6th Workshop on Formal Integrated Development Environment, volume 338, pages 39--45, 2021. [ bib | DOI | full text on HAL ]
[2] Sylvain Conchon, Giorgio Delzanno, and Arnaud Sangnier. Verification of contact tracing protocols via smt-based model checking and counting abstraction. In Stefania Monica and Federico Bergenti, editors, Proceedings of the 36th Italian Conference on Computational Logic, Parma, Italy, September 7-9, 2021, volume 3002 of CEUR Workshop Proceedings, pages 77--91. CEUR-WS.org, 2021. [ bib | .pdf ]
[1] Sylvain Conchon, Alexandrina Korneva, Çagdas Bozman, Mohamed Iguernlala, and Alain Mebsout. Formally documenting tenderbake (short paper). In Bruno Bernardo and Diego Marmsoler, editors, 3rd International Workshop on Formal Methods for Blockchains, FMBC@CAV 2021, July 18-19, 2021, Los Angeles, California, USA (Virtual Conference), volume 95 of OASIcs, pages 4:1--4:9. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. [ bib | DOI ]

PhD theses

[1] Diane Gallois-Wong. Formalisation en Coq des algorithmes de filtre numérique calculés en précision finie. Thèse de doctorat, Université Paris-Saclay, 2021. [ bib | full text on HAL ]

Misc.

Reports

[5] Jean-Christophe Filliâtre. Compte-rendu de fin de projet anr-15-ce25-0008 “vocal”. Technical report, Laboratoire Méthodes Formelles, June 2021. [ bib | full text on HAL ]
[4] Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, and Hiroaki Inoue. Formal analysis of Ladder programs using deductive verification. Research Report RR-9402, Inria, April 2021. [ bib | full text on HAL ]
[3] Benedikt Becker, Cláudio Belo Lourenço, and Claude Marché. Giant-step semantics for the categorisation of counterexamples. Research Report RR-9407, Inria, April 2021. [ bib | full text on HAL ]
[2] Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero. A Coq formalization of Lebesgue integration of nonnegative functions. Research Report RR-9401, Inria, France, 2021. [ bib | full text on HAL ]
Keywords: Lebesgue integration ; Measure theory ; Coq ; Formal proof ; Coq ; Preuve formelle ; Théorie de la mesure ; Intégrale de Lebesgue
[1] Xavier Denis, Jacques-Henri Jourdan, and Claude Marché. The Creusot environment for the deductive verification of Rust programs. Research Report 9448, Inria Saclay - Île de France, 2021. [ bib | full text on HAL ]

Back

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


This page was generated by bibtex2html.