[17]

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 8737 of Lecture Notes in Computer
Science, pages 2536, Wroclaw, Poland, September 2014. Springer.
[ bib 
DOI 
full text on HAL ]
Keywords: Data structure ; Sequence ; Chunk ; Amortization

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

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

[14]

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

[13]

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.
In this article, we describe a simple MLstyle programming language
with mutable state and ghost code. Noninterference 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

[12]

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

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

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 ]

[9]

JeanChristophe Filliâtre.
Deductive program verification with Why3.
In Mathematical Structures of Computation  Formal Proof,
Symbolic Computation and Computer Arithmetic, Lyon, France, February 2014.
Invited talk.
[ bib ]

[8]

Catherine Lelay.
Coq passe le bac.
In JFLA  Journées francophones des langages applicatifs,
Fréjus, France, January 2014.
[ bib ]

[7]

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 ]

[6]

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 ]

[5]

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 ]

[4]

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 ]

[3]

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 ]

[2]

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 ]

[1]

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 ]
