[16] Sylvie Boldo. Formal verification of tricky numerical computations. In 16th GAMM-IMACS 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 25--36, Wroclaw, Poland, September 2014. Springer. [ bib | DOI | full text on HAL ]
Keywords: Data structure ; Sequence ; Chunk ; Amortization
[14] Jean-Christophe 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 1--16, 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 state-of-the-art program verification tools. However, a rigorous definition and treatment of ghost code is surprisingly subtle and few formalizations exist.

In this article, we describe a simple ML-style programming language with mutable state and ghost code. Non-interference is ensured by a type system with effects, which allows, notably, the same data types and functions to be used in both regular and ghost code. We define the procedure of ghost code erasure and we prove its safety using bisimulation. A similar type system, with numerous extensions which we briefly discuss, is implemented in the program verification environment Why3.

Keywords: Why3
[13] Martin Clochard, Jean-Christophe 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 37--51, 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 167--180, Vienna, Austria, July 2014. Springer. [ bib | full text on HAL ]
Keywords: Why3
[11] David Delahaye, Claude Marché, and David Mentré. Le projet BWare : une plate-forme 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 (ANR-12-INSE-0010) 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 290--293, 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 multi-tool 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 189--208, 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 set-theoretic types. part 1: Syntax, semantics, and evaluation. In Proceedings of the 41st ACM SIGPLAN-SIGACT 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. Solar-Lezama. Bridging boolean and quantitative synthesis using smoothed proof search. In Proceedings of the 41st ACM SIGPLAN-SIGACT 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 SIGPLAN-SIGACT 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 Alt-Ergo 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 294--297, 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 Vingt-cinquièmes Journées Francophones des Langages Applicatifs, Fréjus, France, January 2014. [ bib | full text on HAL ]
[2] Jean-Christophe Filliâtre. Le petit guide du bouturage, ou comment réaliser des arbres mutables en OCaml. In Vingt-cinquiè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 ]