2016-conference.bib
@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc 2016-conference.cite -ob 2016-conference.bib -c 'year = 2016 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{pereira16jfla,
topics = {team},
author = {Jean-Christophe Filli\^atre and M\'ario Pereira},
title = {It\'erer avec confiance},
crossref = {jfla16},
hal = {https://hal.inria.fr/hal-01240891}
}
@inproceedings{pereira16nfm,
topics = {team},
author = {Jean-Christophe Filli\^atre and M\'ario Pereira},
title = {A Modular Way to Reason About Iteration},
crossref = {nfm16},
abstract = { In this paper we present an approach to specify
programs performing iterations. The idea is to
specify iteration in terms of the nite sequence of
the elements enumerated so far, and only those. In
particular, we are able to deal with
non-deterministic and possibly innite iteration. We
show how to cope with the issue of an iteration no
longer being consistent with mutable data. We
validate our proposal using the deductive verication
tool Why3 and two iteration paradigms, namely
cursors and higher-order iterators. For each
paradigm, we verify several implementations of
iterators and client code. This is done in a modular
way, i.e., the client code only relies on the
specication of the iteration. },
hal = {https://hal.inria.fr/hal-01281759}
}
@inproceedings{fumex16nfm,
topics = {team},
author = {Fumex, Cl\'ement and Dross, Claire and Gerlach, Jens and March\'e, Claude},
title = {Specification and Proof of High-Level Functional Properties of Bit-Level Programs},
pages = {291--306},
crossref = {nfm16},
hal = {https://hal.inria.fr/hal-01314876}
}
@inproceedings{hauzar16sefm,
topics = {team},
author = {Hauzar, David and March\'e, Claude and Moy, Yannick},
title = {Counterexamples from Proof Failures in {SPARK}},
booktitle = {Software Engineering and Formal Methods},
year = 2016,
pages = {215--233},
doi = {10.1007/978-3-319-41591-8_15},
editor = {De Nicola, Rocco and Eva K\"uhn},
series = {Lecture Notes in Computer Science},
address = {Vienna, Austria},
hal = {https://hal.inria.fr/hal-01314885}
}
@inproceedings{filliatre16,
topics = {team},
author = {Jean-Christophe Filli\^atre and M\'ario Pereira},
title = {Producing All Ideals of a Forest, Formally (Verification Pearl)},
crossref = {vstte16},
hal = {https://hal.inria.fr/hal-01316859}
}
@inproceedings{clochard16,
topics = {team},
author = {Martin Clochard and L\'eon Gondelman and M\'ario Pereira},
title = {The {Matrix} Reproved},
crossref = {vstte16},
hal = {https://hal.inria.fr/hal-01316902}
}
@inproceedings{kosmatov16isola,
topics = {team},
title = {Static versus Dynamic Verification in {Why3}, {Frama-C} and {SPARK
2014}},
author = {Kosmatov, Nikolai and March{\'e}, Claude and Moy, Yannick and
Signoles, Julien},
hal = {https://hal.inria.fr/hal-01344110},
booktitle = {7th International Symposium on Leveraging Applications of Formal
Methods, Verification and Validation (ISoLA)},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
year = 2016,
pages = {461--478},
volume = {9952},
editor = {Tiziana Margaria and Bernhard Steffen},
address = {Corfu, Greece},
month = oct,
doi = {10.1007/978-3-319-47166-2_32}
}
@inproceedings{boldo16nsv,
title = {{Computing a correct and tight rounding error bound using
rounding-to-nearest}},
author = {Boldo, Sylvie},
hal = {https://hal.inria.fr/hal-01377152},
booktitle = {{9th International Workshop on Numerical Software Verification}},
address = {Toronto, Canada},
year = {2016},
month = jul,
pdf = {https://hal.inria.fr/hal-01377152/file/article.pdf},
topics = {team}
}
@inproceedings{boldo16hccv,
title = {{Iterators: where folds fail}},
author = {Boldo, Sylvie},
hal = {https://hal.inria.fr/hal-01377155},
booktitle = {{Workshop on High-Consequence Control Verification}},
address = {Toronto, Canada},
year = {2016},
month = jul,
pdf = {https://hal.inria.fr/hal-01377155/file/abstract.pdf},
topics = {team}
}
@inproceedings{chargueraud:hal-01245865,
topics = {team},
title = {{Higher-Order Representation Predicates in Separation Logic}},
author = {Chargu{\'e}raud, Arthur},
hal = {https://hal.inria.fr/hal-01245865},
booktitle = {{Proceedings of the 5th ACM SIGPLAN Conference on Certified
Programs and Proofs}},
address = {Saint Petersburg, Florida, United States},
year = {2016},
month = jan,
hal_id = {hal-01245865},
hal_version = {v1}
}
@inproceedings{mahboubi16itp,
topics = {team},
title = {Formally Verified Approximations of Definite Integrals},
author = {Mahboubi, Assia and Melquiond, Guillaume and Sibut-Pinote, Thomas},
hal = {https://hal.inria.fr/hal-01289616},
booktitle = {Proceedings of the 7th International Conference on Interactive Theorem Proving},
address = {Nancy, France},
editor = {Jasmin Christian Blanchette and Stephan Merz},
series = {Lecture Notes in Computer Science},
volume = {9807},
year = {2016},
month = aug,
doi = {10.1007/978-3-319-43144-4\_17},
pdf = {https://hal.inria.fr/hal-01289616/file/main.pdf},
hal_id = {hal-01289616},
hal_version = {v2}
}
@inproceedings{acar:hal-01409022,
topics = {team},
title = {Dag-calculus: a calculus for parallel computation},
author = {Acar, Umut A and Chargu{\'e}raud, Arthur and Rainey, Mike and Sieczkowski, Filip},
hal = {https://hal.inria.fr/hal-01409022},
booktitle = {Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP)},
address = {Nara, Japan},
pages = {18--32},
year = 2016,
month = sep,
doi = {10.1145/2951913.2951946}
}
@proceedings{jfla16,
title = {Journ\'ees Francophones des Langages Applicatifs},
year = 2016,
booktitle = {Vingt-septi\`emes Journ\'ees Francophones des Langages Applicatifs},
month = jan,
address = {Saint-Malo, France},
x-international-audience = {no},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA}
}
@proceedings{vstte16,
booktitle = {8th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE)},
month = jul,
year = 2016,
address = {Toronto, Canada},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-cle-support = {VSTTE},
editor = {Sandrine Blazy and Marsha Chechik},
series = {Lecture Notes in Computer Science},
publisher = {Springer}
}
@proceedings{nfm16,
booktitle = {8th NASA Formal Methods Symposium},
address = {Minneapolis, MN, USA},
audience = {internationale},
year = 2016,
month = jun,
editor = {Rayadurgam, Sanjai and Tkachuk, Oksana},
series = {Lecture Notes in Computer Science},
volume = {9690},
publisher = {Springer}
}