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