2017-conference.bib

@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc 2017-conference.cite -ob 2017-conference.bib -c 'year = 2017 and topics : "team" and $type="inproceedings"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}
@inproceedings{jeannerod17jfla,
  author = {Nicolas Jeannerod},
  title = {Le coquillage dans le {CoLiS}-mateur: formalisation d'un langage de programmation de type {Shell}},
  crossref = {jfla17}
}
@inproceedings{boldo:hal-01391578,
  topics = {team},
  title = {{A Coq Formal Proof of the Lax-Milgram theorem}},
  author = {Boldo, Sylvie and Cl{\'e}ment, Fran\c{c}ois and Faissole, Florian
                  and Martin, Vincent and Mayero, Micaela},
  hal = {https://hal.inria.fr/hal-01391578},
  booktitle = {{Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs}},
  series = {CPP 2017},
  location = {Paris, France},
  year = {2017},
  month = jan,
  pages = {79--89},
  pdf = {https://hal.inria.fr/hal-01391578/file/article.pdf},
  doi = {10.1145/3018610.3018625},
  publisher = {ACM},
  address = {New York, NY, USA}
}
@inproceedings{chen17jfla,
  topics = {team},
  author = {Ran Chen and Jean-Jacques L\'evy},
  title = {Une preuve formelle de l'algorithme de {Tarjan-1972} pour trouver les composantes fortement connexes dans un graphe},
  crossref = {jfla17},
  hal = {https://hal.inria.fr/hal-01405424}
}
@inproceedings{clochard17jfla,
  topics = {team},
  title = {{Preuves taill{\'e}es en biseau}},
  author = {Clochard, Martin},
  hal = {https://hal.inria.fr/hal-01404935},
  crossref = {jfla17}
}
@inproceedings{pereira17jfla,
  topics = {team},
  title = {{D{\'e}fonctionnaliser pour prouver}},
  author = {Pereira, M{\'a}rio},
  hal = {https://hal.inria.fr/hal-01378068},
  crossref = {jfla17}
}
@inproceedings{conchon17cav,
  author = {Sylvain Conchon and Mohamed Iguernlala and Kailiang Ji and
                  Guillaume Melquiond and Cl\'ement Fumex},
  topics = {team},
  hal = {https://hal.inria.fr/hal-01522770},
  title = {A Three-tier Strategy for Reasoning about
                  Floating-Point Numbers in {SMT}},
  booktitle = {Computer Aided Verification},
  year = 2017,
  pages = {419--435},
  series = {Lecture Notes in Computer Science},
  volume = 10427,
  doi = {10.1007/978-3-319-63390-9_22}
}
@inproceedings{rieuhelft17jfla,
  topics = {team},
  title = {Result graphs for an abstract interpretation-based static analyzer},
  author = {Rapha{\"e}l Rieu-Helft and Pascal Cuoq},
  crossref = {jfla17}
}
@inproceedings{fumex17vstte,
  topics = {team},
  hal = {https://hal.inria.fr/hal-01534533/},
  author = {Cl\'ement Fumex and Claude March\'e and Yannick Moy},
  title = {Automating the Verification of Floating-Point Programs},
  crossref = {vstte17}
}
@inproceedings{jeannerod17vstte,
  topics = {team},
  hal = {https://hal.inria.fr/hal-01534747},
  author = {Nicolas Jeannerod and Claude March\'e and Ralf Treinen},
  title = {A Formally Verified Interpreter for a Shell-like Programming
                  Language},
  crossref = {vstte17}
}
@inproceedings{boldo17arith,
  topics = {team},
  title = {Round-off Error Analysis of Explicit One-Step Numerical Integration Methods},
  author = {Boldo, Sylvie and Faissole, Florian and Chapoutot, Alexandre},
  hal = {https://hal.archives-ouvertes.fr/hal-01581794},
  booktitle = {24th IEEE Symposium on Computer Arithmetic},
  address = {London, United Kingdom},
  year = {2017},
  month = jul,
  doi = {10.1109/ARITH.2017.22},
  pdf = {https://hal.archives-ouvertes.fr/hal-01581794/file/arith_hal.pdf}
}
@inproceedings{boldo17itp,
  topics = {team},
  title = {Formal Verification of a Floating-Point Expansion Renormalization Algorithm},
  author = {Boldo, Sylvie and Joldes, Mioara and Muller, Jean-Michel and Popescu, Valentina},
  hal = {https://hal.archives-ouvertes.fr/hal-01512417},
  year = {2017},
  month = sep,
  pdf = {https://hal.archives-ouvertes.fr/hal-01512417/file/itp17.pdf},
  booktitle = {Proceedings of the 8th International Conference on Interactive Theorem Proving},
  address = {Brasilia, Brazil}
}
@inproceedings{BCF17b,
  topics = {team},
  title = {Preuve formelle du th{\'e}or{\`e}me de {Lax--Milgram}},
  author = {Boldo, Sylvie and Cl{\'e}ment, Fran\c{c}ois and Faissole, Florian and Martin, Vincent and Mayero, Micaela},
  hal = {https://hal.archives-ouvertes.fr/hal-01581807},
  booktitle = {{16{\`e}mes journ{\'e}es Approches Formelles dans l'Assistance au D{\'e}veloppement de Logiciels}},
  address = {Montpellier, France},
  year = {2017},
  month = jun,
  pdf = {https://hal.archives-ouvertes.fr/hal-01581807/file/article_afadl.pdf}
}
@inproceedings{Faissole17,
  topics = {team},
  title = {{Formalization and closedness of finite dimensional subspaces}},
  author = {Faissole, Florian},
  url = {https://hal.inria.fr/hal-01630411},
  booktitle = {{SYNASC 2017 - 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing}},
  address = {Timisoara, Romania},
  year = {2017},
  month = sep,
  keywords = {filters ; finite dimensional subspaces ; formalization of mathematics ; functional analysis ; formal proof ; Coq},
  pdf = {https://hal.inria.fr/hal-01630411/file/synasc_hal.pdf},
  hal_id = {hal-01630411},
  hal_version = {v1}
}
@inproceedings{chen17vstte,
  topics = {team},
  title = {A Semi-automatic Proof of Strong connectivity},
  author = {Chen, Ran and L{\'e}vy, Jean-Jacques},
  hal = {https://hal.inria.fr/hal-01632947},
  booktitle = {9th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE)},
  address = {Heidelberg, Germany},
  year = 2017,
  month = jul
}
@inproceedings{rieuhelft17vstte,
  topics = {team},
  title = {How to Get an Efficient yet Verified Arbitrary-Precision Integer Library},
  author = {Rieu-Helft, Rapha{\"e}l and March{\'e}, Claude and Melquiond, Guillaume},
  hal = {https://hal.inria.fr/hal-01519732},
  booktitle = {9th Working Conference on Verified Software: Theories, Tools, and Experiments},
  address = {Heidelberg, Germany},
  series = {Lecture Notes in Computer Science},
  volume = 10712,
  year = 2017,
  month = jul,
  pages = {84--101},
  doi = {10.1007/978-3-319-72308-2_6},
  keywords = {arbitrary-precision arithmetic ; deductive program verification ; C language ; Why3 program verifier},
  pdf = {https://hal.inria.fr/hal-01519732/file/main.pdf}
}
@inproceedings{conchon17icfem,
  topics = {team},
  author = {Conchon, Sylvain and Declerck, David and Za{\"i}di, Fatiha},
  editor = {Duan, Zhenhua and Ong, Luke},
  title = {Compiling Parameterized X86-TSO Concurrent Programs to Cubicle-W},
  booktitle = {International Conference on Formal Engineering Methods},
  year = 2017,
  series = {Lecture Notes in Computer Science},
  number = 10610,
  pages = {88--104}
}
@inproceedings{faissole:hal-01405762,
  topics = {team},
  title = {Synthetic topology in {HoTT} for probabilistic programming},
  author = {Faissole, Florian and Spitters, Bas},
  booktitle = {The Third International Workshop on Coq for Programming Languages (CoqPL 2017)},
  address = {Paris, France},
  year = 2017,
  month = jan,
  hal = {https://hal.inria.fr/hal-01405762}
}
@inproceedings{conchon17fmcad,
  topics = {team},
  hal = {https://hal.inria.fr/hal-01927220},
  author = {Sylvain Conchon and
               Amit Goel and
               Sava Krstic and
               Rupak Majumdar and
               Mattias Roux},
  title = {{FAR-Cubicle} - {A} new reachability algorithm for {Cubicle}},
  booktitle = {Formal Methods in Computer Aided Design},
  pages = {172--175},
  year = 2017,
  doi = {10.23919/FMCAD.2017.8102256},
  editor = {Daryl Stewart and Georg Weissenbacher}
}
@inproceedings{filliatre17keysymposium,
  author = {Jean-Christophe Filli\^atre},
  title = {{Why3} --- where programs meet provers},
  booktitle = {KeY Symposium 2017},
  year = 2017,
  month = oct,
  address = {Rastatt, Germany},
  note = {Invited talk},
  topics = {team, lri},
  type_publi = {colloque},
  x-equipes = {demons PROVAL},
  x-type = {invitation},
  x-invited-conference = {yes},
  x-international-audience = {yes}
}
@inproceedings{filliatre17verifythis,
  author = {Jean-Christophe Filli\^atre},
  title = {{Why3} Tutorial},
  booktitle = {VerifyThis 2017},
  year = 2017,
  month = apr,
  address = {Uppsala, Sweden},
  note = {Invited tutorial},
  topics = {team, lri},
  type_publi = {colloque},
  x-equipes = {demons PROVAL},
  x-type = {invitation},
  x-invited-conference = {yes},
  x-international-audience = {yes}
}
@proceedings{jfla17,
  topics = {team},
  hal = {https://hal.inria.fr/hal-01662072},
  title = {Journ\'ees Francophones des Langages Applicatifs},
  editor = {Boldo, Sylvie and Signoles, Julien},
  year = 2017,
  booktitle = {Vingt-huiti\`emes Journ\'ees Francophones des Langages Applicatifs},
  month = jan,
  address = {Gourette, France},
  x-international-audience = {no},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {JFLA}
}
@proceedings{vstte17,
  topics = {team},
  hal = {https://hal.inria.fr/hal-01670145},
  title = {Verified Software: Theories, Tools, and Experiments. Revised Selected Papers Presented at the 9th International Conference {VSTTE}},
  booktitle = {Verified Software: Theories, Tools, and Experiments. Revised Selected Papers Presented at the 9th International Conference {VSTTE}},
  month = dec,
  year = 2017,
  address = {Heidelberg, Germany},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {VSTTE},
  editor = {Andrei Paskevich and Thomas Wies},
  series = {Lecture Notes in Computer Science},
  number = 10712,
  publisher = {Springer}
}