|
[11]
|
Jean-Christophe Filliâtre and Andrei Paskevich.
Abstraction and genericity in Why3.
In Tiziana Margaria and Bernhard Steffen, editors, 9th
International Symposium On Leveraging Applications of Formal Methods,
Verification and Validation (ISoLA), volume 12476 of Lecture Notes in
Computer Science, pages 122--142, Rhodes, Greece, October 2020. Springer.
See also https://usr.lmf.cnrs.fr/~jcf/isola-2020/.
[ bib |
full text on HAL ]
|
|
[10]
|
Jean-Christophe Filliâtre.
A Coq retrospective - at the heart of Coq architecture, the
genesis of version 7.0.
In The Coq Workshop 2020, virtual, July 2020.
Invited talk.
[ bib |
full text on HAL |
http ]
|
|
[9]
|
Diego Diverio, Cláudio Belo Lourenço, and Claude Marché.
“You-Know-Why”: an early-stage prototype of a key server
developed using Why3.
In VerifyThis Long-term Challenge 2020: Proceedings of the
Online-Event, pages 4--7, Dublin, Ireland, April 2020. Karlsruhe Institute
of Technology.
[ bib |
DOI |
full text on HAL ]
|
|
[8]
|
Martin Clochard, Claude Marché, and Andrei Paskevich.
Deductive verification with ghost monitors.
In Principles of Programming Languages, New Orleans, United
States, 2020.
[ bib |
DOI |
full text on HAL ]
|
|
[7]
|
Jean-Christophe Filliâtre.
Mesurer la hauteur d'un arbre.
In Zaynah Dargaye and Yann Régis-Gianas, editors,
Trente-et-unièmes Journées Francophones des Langages Applicatifs,
Gruissan, France, January 2020.
https://usr.lmf.cnrs.fr/~jcf/hauteur/.
[ bib |
full text on HAL |
Slides ]
|
|
[6]
|
Quentin Garchery, Chantal Keller, Claude Marché, and Andrei Paskevich.
Des transformations logiques passent leur certicat.
In Zaynah Dargaye and Yann Régis-Gianas, editors,
Trente-et-unièmes Journées Francophones des Langages Applicatifs,
Gruissan, France, January 2020.
[ bib |
full text on HAL ]
|
|
[5]
|
Benedikt Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas,
Mihaela Sighireanu, and Ralf Treinen.
Analysing installation scenarios of Debian packages.
In Tools and Algorithms for the Construction and Analysis of
Systems, volume 12079 of Lecture Notes in Computer Science, pages
235--253, 2020.
[ bib |
DOI |
full text on HAL ]
|
|
[4]
|
Guillaume Melquiond and Raphaël Rieu-Helft.
WhyMP, a formally verified arbitrary-precision integer library.
In 45th International Symposium on Symbolic and Algebraic
Computation (ISSAC), pages 352--359, 2020.
[ bib |
DOI |
full text on HAL ]
Keywords: Integer arithmetic ; Deductive program verification ; Mathematical library
|
|
[3]
|
Sylvie Boldo, Diane Gallois-Wong, and Thibault Hilaire.
A correctly-rounded fixed-point-arithmetic dot-product algorithm.
In 27th IEEE Symposium on Computer Arithmetic (ARITH), pages
9--16. IEEE, 2020.
[ bib |
DOI |
full text on HAL ]
Keywords: Dot Product ; Sum-of-Products ; Correct Round- ing ; Odd Rounding ; Fixed-Point Arithmetic
|
|
[2]
|
Thierry Lecomte, David Déharbe, Denis Sabatier, Etienne Prun, Patrick
Péronne, Emmanuel Chailloux, Steven Varoumas, Adilla Susungi, and Sylvain
Conchon.
Low cost high integrity platform.
In 10th European Congress on Embedded Real Time Systems (ERTS),
Toulouse, France, 2020.
[ bib |
full text on HAL ]
Keywords: Safety ; Certification ; Formal methods
|
|
[1]
|
Georges-Axel Jaloyan, Claire Dross, Maroua Maalej, Yannick Moy, and Andrei
Paskevich.
Verification of programs with pointers in SPARK.
In Formal Methods and Software Engineering (ICFEM), pages
55--72, 2020.
[ bib |
DOI |
full text on HAL ]
|