Wiki Agenda Contact English version

Publications 2022

Retour

Livres / Revues / Conférences / Thèses / Divers / Rapports

Livres et chapitres de livres

[1] Thibaut Balabonski, Sylvain Conchon, Jean-Christophe Filliâtre, Kim Nguyen, and Laurent Sartre. Informatique - MP2I/MPI - CPGE 1re et 2e années - Cours et exercices corrigés. Ellipses, 2022. [ bib | full text on HAL ]

Revues

[4] Louise Ben Salem-Knapp, Sylvie Boldo, and William Weens. Bounding the round-off error of the upwind scheme for advection. IEEE Transactions on Emerging Topics in Computing, 10(3), 2022. [ bib | DOI | full text on HAL ]
Keywords: Round-off error ; Floating-Point ; Numerical Scheme ; Advection ; Hydrodynamics
[3] Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, and Hiroaki Inoue. Automated formal analysis of temporal properties of Ladder programs. International Journal on Software Tools for Technology Transfer, 24(6):977--997, 2022. [ bib | DOI | full text on HAL ]
Keywords: Ladder language for programming PLCs ; Timing charts ; Formal specification ; Deductive verification ; Why3 environment
[2] Benedikt Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, and Ralf Treinen. The CoLiS platform for the analysis of maintainer scripts in Debian software packages. International Journal on Software Tools for Technology Transfer, 2022. [ bib | full text on HAL ]
[1] Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero. A Coq formalization of Lebesgue integration of nonnegative functions. Journal of Automated Reasoning, 66:175--213, 2022. [ bib | DOI | full text on HAL ]

Conférences

[7] Jean-Christophe Filliâtre and Clément Pascutto. Optimizing prestate copies in runtime verification of function postconditions. In 22nd International Conference on Runtime Verification, 2022. [ bib | full text on HAL ]
[6] Xavier Denis, Jacques-Henri Jourdan, and Claude Marché. Creusot: a foundry for the deductive verication of Rust programs. In International Conference on Formal Engineering Methods - ICFEM, Lecture Notes in Computer Science, Madrid, Spain, 2022. Springer. [ bib | full text on HAL ]
Keywords: Rust programming language ; Deductive program verification ; Aliasing and Ownership ; Prophecies ; Traits
[5] Yusuke Matsushita, Xavier Denis, Jacques-Henri Jourdan, and Derek Dreyer. RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code. In International Conference on Programming Language Design and Implementation, pages 841--856. ACM, 2022. [ bib | DOI | full text on HAL ]
[4] Thomas Van Strydonck, Aïna Linn Georges, Armaël Guéneau, Alix Trieu, Amin Timany, Frank Piessens, Lars Birkedal, and Dominique Devriese. Proving full-system security properties under multiple attacker models on capability machines. In CSF 2022 - 35th IEEE Computer Security Foundations Symposium, 2022. [ bib | full text on HAL ]
[3] Léo Andrès, Raja Boujbel, Louis Gesbert, and Dario Pinto. Connecter l'écosystème OCaml à Software Heritage via opam. In Chantal Keller and Timothy Bourke, editors, 33èmes Journées Francophones des Langages Applicatifs, pages 227--234, 2022. [ bib | full text on HAL ]
[2] Çagdas Bozman, Mohamed Iguernlala, Michael Laporte, Maxime Levillain, Alain Mebsout, and Sylvain Conchon. Jouez à faire consensus avec MITTEN (démonstration). In Chantal Keller and Timothy Bourke, editors, 33èmes Journées Francophones des Langages Applicatifs, pages 248--250, 2022. [ bib | full text on HAL ]
[1] Sylvain Conchon. Some insights on open problems in blockchains: Explorative tracks for tezos (invited talk). In Sara Tucci Piergiovanni and Natacha Crooks, editors, 5th International Symposium on Foundations and Applications of Blockchain 2022, FAB 2022, June 3, 2022, Berkeley, CA, USA, volume 101 of OASIcs, pages 2:1--2:1. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. [ bib | DOI ]

Thèses

[1] Quentin Garchery. Certification de la transformation de tâches de preuve. Thèse de doctorat, Université Paris-Saclay, 2022. [ bib | full text on HAL ]

Divers

[2] Sylvie Boldo, François Clément, and Louise Leclerc. A Coq formalization of the Bochner integral. working paper or preprint, 2022. [ bib | full text on HAL ]
[1] Josué Moreau. Compilation formellement vérifiée d'un langage pour le calcul formel. working paper or preprint, 2022. [ bib | full text on HAL ]

Rapports


Retour

Livres / Revues / Conférences / Thèses / Divers / Rapports


This page was generated by bibtex2html.