Publications 2014
BackBooks / Journals / Conferences / PhD theses / Misc. / Reports
Books and book chapters
[2]  Sylvie Boldo. Même les ordinateurs font des erreurs ! In Martin Andler, Liliane Bel, Sylvie BenzoniGavage, Thierry Goudon, Cyril Imbert, and Antoine Rousseau, editors, Brèves de maths, pages 136137. Nouveau Monde Editions, October 2014. [ bib  full text on HAL  http ] 
[1]  Sylvain Conchon and JeanChristophe Filliâtre. Apprendre à programmer avec OCaml. Algorithmes et structures de données. Eyrolles, September 2014. [ bib  full text on HAL  http ] 
Journals
[4]  Sylvie Boldo and JeanMichel Muller. Des ordinateurs capables de calculer plus juste. La Recherche, 492:4652, October 2014. [ bib  full text on HAL ] 
[3] 
Claude Marché.
Verification of the functional behavior of a floatingpoint program:
an industrial case study.
Science of Computer Programming, 96(3):279296, March 2014.
[ bib 
DOI 
full text on HAL 
.pdf ]
We report on a case study that was conducted as part of an industrial research project on static analysis of critical C code. The example program considered in this paper is an excerpt of an industrial code, only slightly modified for confidentiality reasons, involving floatingpoint computations. The objective was to establish a property on the functional behavior of this code, taking into account rounding errors made during computations. The property is formalized using ACSL, the behavioral specification language available inside the FramaC environment, and it is verified by automated theorem proving

[2]  Sylvie Boldo, François Clément, JeanChristophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program. Computers and Mathematics with Applications, 68(3):325352, 2014. [ bib  DOI  full text on HAL  http ] 
[1] 
Érik MartinDorel, Guillaume Hanrot, Micaela Mayero, and Laurent Théry.
Formally verified certificate checkers for hardesttoround
computation.
Journal of Automated Reasoning, pages 129, 2014.
[ bib 
DOI 
full text on HAL ]
Keywords: Formal proofs; Certificate checkers; Hensel’s lemma; Modular arithmetic 
Conferences
[16]  Sylvie Boldo. Formal verification of tricky numerical computations. In 16th GAMMIMACS International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics, Würzburg, Germany, September 2014. Invited talk. [ bib  full text on HAL  http ] 
[15] 
Umut A. Acar, Arthur Charguéraud, and Mike Rainey.
Theory and practice of chunked sequences.
In AndreasS. Schulz and Dorothea Wagner, editors, European
Symposium on Algorithms, volume Lecture Notes in Computer Science, pages
2536, Wroclaw, Poland, September 2014. Springer.
[ bib 
DOI 
full text on HAL ]
Keywords: Data structure ; Sequence ; Chunk ; Amortization 
[14] 
JeanChristophe Filliâtre, Léon Gondelman, and Andrei Paskevich.
The spirit of ghost code.
In Armin Biere and Roderick Bloem, editors, 26th International
Conference on Computer Aided Verification, volume 8859 of Lecture Notes
in Computer Science, pages 116, Vienna, Austria, July 2014. Springer.
[ bib 
full text on HAL 
.pdf ]
In the context of deductive program verification, ghost code is part of the program that is added for the purpose of specification. Ghost code must not interfere with regular code, in the sense that it can be erased without any observable difference in the program outcome. In particular, ghost data cannot participate in regular computations and ghost code cannot mutate regular data or diverge. The idea exists in the folklore since the early notion of auxiliary variables and is implemented in many stateoftheart program verification tools. However, a rigorous definition and treatment of ghost code is surprisingly subtle and few formalizations exist. Keywords: Why3 
[13] 
Martin Clochard, JeanChristophe Filliâtre, Claude Marché, and Andrei
Paskevich.
Formalizing semantics with an automatic program verifier.
In Dimitra Giannakopoulou and Daniel Kroening, editors, 6th
Working Conference on Verified Software: Theories, Tools and Experiments
(VSTTE), volume 8471 of Lecture Notes in Computer Science, pages
3751, Vienna, Austria, July 2014. Springer.
[ bib 
full text on HAL ]
Keywords: Why3 
[12] 
Martin Clochard.
Automatically verified implementation of data structures based on
AVL trees.
In Dimitra Giannakopoulou and Daniel Kroening, editors, 6th
Working Conference on Verified Software: Theories, Tools and Experiments
(VSTTE), volume 8471 of Lecture Notes in Computer Science, pages
167180, Vienna, Austria, July 2014. Springer.
[ bib 
full text on HAL ]
Keywords: Why3 
[11] 
David Delahaye, Claude Marché, and David Mentré.
Le projet BWare : une plateforme pour la vérification
automatique d'obligations de preuve B.
In Approches Formelles dans l'Assistance au Développement de
Logiciels (AFADL), Paris, France, June 2014. EasyChair.
[ bib 
full text on HAL ]
Le projet de recherche industrielle BWare (ANR12INSE0010) est financé pour 4 ans par le programme Ingénierie Numérique & Sécurité (INS) de l'Agence Nationale de la Recherche (ANR) et a débuté en septembre 2012 (voir le site web du projet : http://bware.lri.fr). Le consortium du projet BWare associe les partenaires académiques Cedric, LRI, et Inria, ainsi que les partenaires industriels Mitsubishi Electric R&D Centre Europe (MERCE), ClearSy, et OCamlPro

[10] 
David Delahaye, Catherine Dubois, Claude Marché, and David Mentré.
The BWare project: Building a proof platform for the automated
verification of B proof obligations.
In Abstract State Machines, Alloy, B, VDM, and Z (ABZ), volume
8477 of Lecture Notes in Computer Science, pages 290293, Toulouse,
France, June 2014. Springer.
[ bib 
full text on HAL ]
We introduce BWare, an industrial research project that aims to provide a mechanized framework to support the automated veri cation of proof obligations coming from the development of industrial applications using the B method and requiring high integrity. The methodology adopted consists in building a generic verification platform relying on di erent theorem provers, such as rst order provers and SMT (Satisfiability Modulo Theories) solvers. Beyond the multitool aspect of our methodology, the originality of this project also resides in the requirement for the veri cation tools to produce proof objects, which are to be checked independently. In this paper, we present some preliminary results of BWare, as well as some current major lines of work

[9]  Véronique Benzaken, Évelyne Contejean, and Stefania Dumbrava. A Coq formalization of the relational data model. In Z. Shao, editor, European Symposium on Programming, LNCS 8410, Lecture Notes in Computer Science, pages 189208, Grenoble, April 2014. Springer. [ bib  full text on HAL ] 
[8]  Martin Clochard, Claude Marché, and Andrei Paskevich. Verified programs with binders. In Programming Languages meets Program Verification (PLPV). ACM Press, 2014. [ bib  full text on HAL ] 
[7]  Giuseppe Castagna, Hyeonseung Im, Sergeï Lenglet, Kim Nguyen, Luca Padovani, and Zhiwu Xu. Polymorphic functions with settheoretic types. part 1: Syntax, semantics, and evaluation. In Proceedings of the 41st ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, San Diego, USA, January 2014. ACM Press. [ bib  full text on HAL ] 
[6]  M. Clochard, S. Chaudhuri, and A. SolarLezama. Bridging boolean and quantitative synthesis using smoothed proof search. In Proceedings of the 41st ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, San Diego, USA, January 2014. ACM Press. [ bib  full text on HAL ] 
[5]  M. Bodin, A. Charguéraud, D. Filaretti, P. Gardner, S. Maffeis, D. Naudziuniene, A. Schmitt, and G. Smith. A trusted mechanised JavaScript specification. In Proceedings of the 41st ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, San Diego, USA, January 2014. ACM Press. [ bib  full text on HAL ] 
[4]  Sylvain Conchon and Mohamed Iguernelala. Tuning the AltErgo SMT solver for B proof obligations. In Abstract State Machines, Alloy, B, VDM, and Z (ABZ), volume 8477 of Lecture Notes in Computer Science, pages 294297, Toulouse, France, June 2014. Springer. [ bib  DOI  full text on HAL ] 
[3]  Sylvain Conchon, David Declerck, Luc Maranget, and Alain Mebsout. Vérification de programmes C concurrents avec Cubicle : Enfoncer les barrières. In Vingtcinquièmes Journées Francophones des Langages Applicatifs, Fréjus, France, January 2014. [ bib  full text on HAL ] 
[2]  JeanChristophe Filliâtre. Le petit guide du bouturage, ou comment réaliser des arbres mutables en OCaml. In Vingtcinquièmes Journées Francophones des Langages Applicatifs, Fréjus, France, January 2014. https://www.lri.fr/~filliatr/publis/bouturage.pdf. [ bib ] 
[1]  Catherine Lelay. Coq passe le bac. In JFLA  Journées francophones des langages applicatifs, Fréjus, France, January 2014. [ bib ] 
PhD theses
[4]  Sylvie Boldo. Deductive Formal Verification: How To Make Your FloatingPoint Programs Behave. Thèse d'habilitation, Université ParisSud, October 2014. [ bib  full text on HAL ] 
[3]  Alain Mebsout. Invariants inference for model checking of parameterized systems. Thèse de doctorat, Université ParisSud, September 2014. [ bib  full text on HAL ] 
[2]  Évelyne Contejean. Facettes de la preuve, Jeux de reflets entre démonstration automatique et preuve assisté. Thèse d'habilitation, Université ParisSud, June 2014. https://www.lri.fr/~contejea/dossiers/hdr/hdr.pdf. [ bib  full text on HAL ] 
[1]  Claire Dross. Generic Decision Procedures for Axiomatic FirstOrder Theories. Thèse de doctorat, Université ParisSud, April 2014. [ bib  full text on HAL ] 
Misc.
Reports
[1]  Jacques Charles Mbiada Ndjanda. FCLLVM: un compilateur intégré à l'environnement FramaC. Master's thesis, Université ParisDiderot, 2014. https://www.lri.fr/~jmbiadan/public/cea_intership_v1.pdf. [ bib ] 
Back
Books / Journals / Conferences / PhD theses / Misc. / Reports
This page was generated by bibtex2html.