[16]
|
Jean-Christophe Filliâtre.
Deductive verification of OCaml libraries.
In 15th International Conference on integrated Formal Methods,
Bergen, Norway, December 2019.
Invited talk.
[ bib |
full text on HAL ]
|
[15]
|
Arthur Charguéraud, Jean-Christophe Filliâtre, Cláudio Belo Lourenço,
and Mário Pereira.
GOSPEL --- providing OCaml with a formal specification language.
In Annabelle McIver and Maurice ter Beek, editors, FM 2019 23rd
International Symposium on Formal Methods, Porto, Portugal, October 2019.
[ bib |
full text on HAL ]
|
[14]
|
Florian Steinberg, Holger Thies, and Laurent Théry.
Quantitative continuity and Computable Analysis in Coq.
In ITP 2019 - Tenth International Conference on Interactive
Theorem Proving, Portland, United States, September 2019.
The version accepted to the conference can be accessed at
https://drops.dagstuhl.de/opus/volltexte/2019/11083/.
[ bib |
DOI |
full text on HAL ]
Keywords: Computable analysis ; Coq ; Contionuous functionals ; Discontinuity ; Closed choice on the natura
|
[13]
|
Benedikt Becker and Claude Marché.
Ghost code in action: Automated verification of a symbolic
interpreter.
In Supratik Chakraborty and Jorge A.Navas, editors, Verified
Software: Tools, Techniques and Experiments, volume 12031 of Lecture
Notes in Computer Science, New York, United States, July 2019.
[ bib |
DOI |
full text on HAL ]
|
[12]
|
Jean-Christophe Filliâtre.
The Why3 tool for deductive verification and verified OCaml
libraries.
In Frama-C & SPARK Day 2019, Paris, France, June 2019.
Invited talk.
[ bib ]
|
[11]
|
Guillaume Melquiond and Raphaël Rieu-Helft.
Formal verification of a state-of-the-art integer square root.
In Symposium on Computer Arithmetic, pages 183--186, Kyoto,
Japan, June 2019.
[ bib |
full text on HAL ]
|
[10]
|
Florian 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.
[ bib |
full text on HAL ]
|
[9]
|
Thibault Hilaire, Hacène Ouzia, and Benoit Lopez.
Optimal Word-Length Allocation for the Fixed-Point Implementation of
Linear Filters and Controllers.
In ARITH 2019 - IEEE 26th Symposium on Computer Arithmetic,
pages 175--182, Kyoto, Japan, June 2019. IEEE.
[ bib |
DOI |
full text on HAL |
.pdf ]
Keywords: fixed-point arithmetic ; word-length allocation
|
[8]
|
Cláudio Belo Lourenço, Maria João Frade, and Jorge 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.
[ bib |
full text on HAL |
.pdf ]
|
[7]
|
Akitoshi Kawamura, Florian Steinberg, and Holger Thies.
Second-order linear-time computability with applications to
computable analysis.
In 15th Annual Conference Theory and Applications of Models of
Computation, volume 11436 of Lecture Notes in Computer Science, pages
337--358, Tokyo, Japan, April 2019. Springer.
[ bib |
full text on HAL ]
|
[6]
|
Raphaël Rieu-Helft.
Un mécanisme de preuve par réflexion pour Why3 et son
application aux algorithmes de GMP.
In Nicolas Magaud and Zaynah Dargaye, editors, Trentièmes
Journées Francophones des Langages Applicatifs, Les Rousses, France,
January 2019.
[ bib |
full text on HAL ]
|
[5]
|
Diane Gallois-Wong.
Formalisation en Coq d'algorithmes de filtres numériques.
In 30èmes Journées Francophones des Langages
Applicatifs, January 2019.
[ bib |
full text on HAL ]
|
[4]
|
Jean-Christophe Filliâtre.
Retour sur 25 ans de programmation avec OCaml.
In Nicolas Magaud and Zaynah Dargaye, editors, Trentièmes
Journées Francophones des Langages Applicatifs, Les Rousses, France,
January 2019.
Séminaire invité.
[ bib |
full text on HAL ]
|
[3]
|
Valentin Blot, Amina Bousalem, Quentin Garchery, and Chantal Keller.
SMTCoq: automatisation expressive et extensible dans Coq.
In Nicolas Magaud and Zaynah Dargaye, editors, Trentièmes
Journées Francophones des Langages Applicatifs, Les Rousses, France,
January 2019.
[ bib |
full text on HAL ]
|
[2]
|
Guillaume Melquiond.
Computer arithmetic and formal proofs.
In Nicolas Magaud and Zaynah Dargaye, editors, Trentièmes
Journées Francophones des Langages Applicatifs, Les Rousses, France,
January 2019.
[ bib |
full text on HAL ]
|
[1]
|
Sylvain Conchon and Mattias Roux.
Reasoning about universal cubes in MCMT.
In Yamine Aït Ameur and Shengchao Qin, editors,
International Conference on Formal Engineering Methods, volume 11852 of
Lecture Notes in Computer Science, pages 270--285. Springer, 2019.
[ bib |
full text on HAL ]
|
[5]
|
Nicolas Jeannerod, Yann Régis-Gianas, Claude Marché, Mihaela
Sighireanu, and Ralf Treinen.
Specification of UNIX utilities.
Technical report, HAL Archives Ouvertes, October 2019.
[ bib |
full text on HAL ]
|
[4]
|
Benedikt Becker, Claude Marché, Nicolas Jeannerod, and Ralf Treinen.
Revision 2 of CoLiS language: formal syntax, semantics, concrete
and symbolic interpreters.
Technical report, HAL Archives Ouvertes, October 2019.
[ bib |
full text on HAL ]
|
[3]
|
Léo Andrès.
Vérification par preuve formelle de propriétés fonctionnelles
d'algorithme de classification.
Rapport de stage de M1, Université Paris Sud, August 2019.
[ bib |
full text on HAL ]
|
[2]
|
The Coq Development Team.
The Coq Proof Assistant Reference Manual -- Version V8.9,
2019.
http://coq.inria.fr.
[ bib |
http ]
|
[1]
|
Marieke Huisman, Rosemary Monahan, Peter Müller, Andrei Paskevich, and
Gidon Ernst.
Verifythis 2018: A program verification competition.
Research report, Université Paris-Saclay, January 2019.
[ bib |
full text on HAL ]
|