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}
}