2014-conference.bib

@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -oc 2014-conference.cite -ob 2014-conference.bib -c 'year = 2014 and topics : "team" and $type="inproceedings"' /home/marche/biblio/abbrevs.bib /home/marche/biblio/demons.bib /home/marche/biblio/demons2.bib /home/marche/biblio/demons3.bib /home/marche/biblio/team.bib /home/marche/biblio/crossrefs.bib}}
@inproceedings{boldo14scan,
  hal = {https://hal.inria.fr/hal-01088692},
  title = {Formal verification of tricky numerical computations},
  author = {Sylvie Boldo},
  year = 2014,
  booktitle = {16th GAMM-IMACS International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics},
  address = {Würzburg, Germany},
  month = sep,
  note = {Invited talk},
  url = {http://www.scan2014.uni-wuerzburg.de/book_of_abstracts/},
  topics = {team,lri},
  type_publi = {colloque}
}
@inproceedings{benzaken14esop,
  hal = {http://hal.inria.fr/hal-00924156},
  author = {V\'eronique Benzaken and \'Evelyne Contejean and Stefania Dumbrava},
  title = {A {Coq} Formalization of the Relational Data Model},
  crossref = {esop2014},
  year = 2014,
  month = apr,
  editor = {Z. Shao},
  booktitle = {European Symposium on Programming, LNCS 8410},
  pages = {189-208},
  type_publi = {icolcomlec},
  topics = {team},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-support = {actes}
}
@inproceedings{clochard14plpv,
  hal = {http://hal.inria.fr/hal-00913431},
  topics = {team},
  author = {Martin Clochard and Claude March\'e and Andrei Paskevich},
  title = {Verified Programs with Binders},
  booktitle = {Programming Languages meets Program Verification (PLPV)},
  year = 2014,
  publisher = {ACM Press},
  type_digiteo = {conf_isbn},
  type_publi = {colloque},
  x-equipes = {demons Toccata},
  x-support = {actes},
  x-cle-support = {PLPV}
}
@inproceedings{castagna14popl,
  hal = {http://hal.archives-ouvertes.fr/hal-00880744},
  topics = {team},
  author = {Giuseppe Castagna and Hyeonseung Im and Serge{\"\i} Lenglet and Kim Nguyen and Luca Padovani and Zhiwu Xu},
  title = {Polymorphic Functions with Set-Theoretic Types. Part 1: Syntax, Semantics, and Evaluation},
  crossref = {popl2014}
}
@inproceedings{clochard14popl,
  hal = {http://hal.inria.fr/hal-00920955},
  topics = {team},
  author = {M. Clochard and S. Chaudhuri and A. Solar-Lezama},
  title = {Bridging Boolean and Quantitative Synthesis Using Smoothed Proof Search},
  crossref = {popl2014}
}
@inproceedings{bodin14popl,
  hal = {http://hal.inria.fr/hal-00910135},
  topics = {team},
  author = {M. Bodin and A. Chargu{\'e}raud and D. Filaretti and P. Gardner and S. Maffeis and D. Naudziuniene and A. Schmitt and G. Smith},
  title = {A Trusted Mechanised {JavaScript} Specification},
  crossref = {popl2014}
}
@inproceedings{filliatre14cav,
  author = {Jean-Christophe Filli\^atre and L\'eon
            Gondelman and Andrei Paskevich},
  title = {The Spirit of Ghost Code},
  pages = {1--16},
  crossref = {cav2014},
  topics = {team},
  keywords = {Why3},
  type_publi = {icolcomlec},
  x-international-audience = {yes},
  x-proceedings = {yes},
  hal_id = {hal-00873187},
  hal = {http://hal.archives-ouvertes.fr/hal-00873187/en/},
  pdf = {http://hal.archives-ouvertes.fr/hal-00873187/PDF/main.pdf},
  abstract = {
  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.
  }
}
@inproceedings{delahaye14afadl,
  topics = {team},
  hal_id = {hal-00998094},
  hal = {http://hal.inria.fr/hal-00998094/en/},
  title = {Le projet {BWare} : une plate-forme pour la v{\'e}rification automatique d'obligations de preuve {B}},
  author = {Delahaye, David and March{\'e}, Claude and Mentr{\'e}, David},
  abstract = {Le projet de recherche industrielle BWare (ANR-12-INSE-0010) est financ{\'e} pour 4 ans par le programme \emph{Ing{\'e}nierie Num{\'e}rique \& S{\'e}curit{\'e}} (INS) de l'Agence Nationale de la Recherche (ANR) et a d{\'e}but{\'e} en septembre 2012 (voir le site web du projet : \url{http://bware.lri.fr}). Le consortium du projet BWare associe les partenaires acad{\'e}miques Cedric, LRI, et Inria, ainsi que les partenaires industriels Mitsubishi Electric R\&D Centre Europe (MERCE), ClearSy, et OCamlPro},
  booktitle = {Approches Formelles dans l'Assistance au D{\'e}veloppement de Logiciels (AFADL)},
  publisher = {EasyChair},
  address = {Paris, France},
  audience = {nationale},
  year = 2014,
  month = jun
}
@inproceedings{delahaye14abz,
  topics = {team},
  crossref = {abz2014},
  hal_id = {hal-00998092},
  hal = {http://hal.inria.fr/hal-00998092/en/},
  title = {The {BWare} Project: Building a Proof Platform for the Automated Verification of {B} Proof Obligations},
  author = {Delahaye, David and Dubois, Catherine and March{\'e}, Claude and Mentr{\'e}, David},
  abstract = { 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},
  language = {Anglais},
  affiliation = {Centre d'Etude et De Recherche en Informatique du Cnam - CEDRIC , TOCCATA - INRIA Saclay - {\^I}le-de-France , Laboratoire de Recherche en Informatique - LRI , Mitsubishi Electric R\&D Centre Europe [France] - MERCE-France},
  pages = {290--293}
}
@inproceedings{conchon14abz,
  topics = {team},
  hal = {https://hal.inria.fr/hal-01093000},
  author = {Sylvain Conchon and Mohamed Iguernelala},
  title = {Tuning the {Alt-Ergo} {SMT} Solver for {B} Proof Obligations},
  pages = {294--297},
  year = 2014,
  crossref = {abz2014},
  doi = {10.1007/978-3-662-43652-3_27}
}
@inproceedings{cfmp14vstte,
  hal = {http://hal.inria.fr/hal-01067197},
  author = {Martin Clochard and Jean-Christophe
  Filli\^atre and Claude March\'e and Andrei Paskevich},
  title = {Formalizing Semantics with an Automatic Program
  Verifier},
  pages = {37--51},
  crossref = {vstte14},
  topics = {team,lri},
  keywords = {Why3},
  type_publi = {icolcomlec},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{clochard14vstte,
  hal = {http://hal.inria.fr/hal-01067217},
  author = {Martin Clochard},
  title = {Automatically verified implementation of data structures
                  based on {AVL} trees},
  pages = {167--180},
  crossref = {vstte14},
  topics = {team,lri},
  keywords = {Why3},
  type_publi = {icolcomlec},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{conchon14jfla,
  hal = {https://hal.inria.fr/hal-01088655},
  topics = {team},
  author = {Sylvain Conchon and David Declerck and Luc Maranget and Alain Mebsout},
  title = {Vérification de programmes {C} concurrents avec {Cubicle} : Enfoncer les barrières},
  crossref = {jfla14}
}
@inproceedings{acar14esa,
  topics = {team},
  title = {Theory and Practice of Chunked Sequences},
  author = {Acar, Umut A. and Chargu{\'e}raud, Arthur and Rainey, Mike},
  hal = {https://hal.inria.fr/hal-01087245},
  booktitle = {European Symposium on Algorithms},
  address = {Wroclaw, Poland},
  editor = {Schulz, AndreasS. and Wagner, Dorothea},
  publisher = {Springer},
  volume = {Lecture Notes in Computer Science},
  number = 8737,
  pages = {25--36},
  year = 2014,
  month = sep,
  doi = {10.1007/978-3-662-44777-2_3},
  keywords = {Data structure ;  Sequence ;  Chunk ;  Amortization}
}
@inproceedings{lelay14jfla,
  topics = {team},
  title = {{Coq passe le bac}},
  author = {Lelay, Catherine},
  booktitle = {{JFLA - Journ{\'e}es francophones des langages applicatifs}},
  address = {Fr{\'e}jus, France},
  year = {2014},
  month = jan,
  x-proceedings = {no},
  x-international-audience = {no},
  x-editorial-board = {yes},
  x-invited-conference = {yes},
  x-scientific-popularization = {no}
}
@proceedings{popl2014,
  title = {Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  year = 2014,
  booktitle = {Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  address = {San Diego, USA},
  month = jan,
  publisher = {ACM Press}
}
@proceedings{cav2014,
  editor = {Armin Biere and Roderick Bloem},
  title = {Computer Aided Verification},
  booktitle = {26th International Conference on Computer Aided Verification},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = 8859,
  address = {Vienna, Austria},
  month = jul,
  year = 2014
}
@proceedings{jfla14,
  title = {Journ\'ees Francophones des Langages Applicatifs},
  year = 2014,
  booktitle = {Vingt-cinqui\`emes Journ\'ees Francophones des Langages Applicatifs},
  month = jan,
  address = {Fr\'ejus, France},
  x-international-audience = {no},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {JFLA}
}
@proceedings{esop2014,
  title = {23rd European Symposium on Programming (ESOP)},
  year = 2014,
  booktitle = {ESOP},
  editor = {Zhong Shao},
  series = {Lecture Notes in Computer Science},
  address = {Grenoble},
  month = apr,
  publisher = {Springer}
}
@proceedings{vstte14,
  booktitle = {6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE)},
  month = jul,
  year = 2014,
  address = {Vienna, Austria},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {VSTTE},
  editor = {Dimitra Giannakopoulou and Daniel Kroening},
  series = {Lecture Notes in Computer Science},
  volume = 8471,
  publisher = {Springer}
}
@proceedings{abz2014,
  booktitle = {Abstract State Machines, Alloy, B, VDM, and Z (ABZ)},
  publisher = {Springer},
  address = {Toulouse, France},
  volume = 8477,
  series = {Lecture Notes in Computer Science},
  audience = {internationale},
  year = 2014,
  month = jun
}