publis.bib

@inproceedings{alt-ergo2.2,
  author = {{Albin Coquereau, Sylvain Conchon, Mohamed Iguernlala, Alain Mebsout}},
  title = {{Alt-Ergo 2.2}},
  booktitle = {International Workshop on Satisfiability
Modulo Theories (SMT 2018), to appear},
  month = jul,
  year = {2018},
  url = {https://github.com/OCamlPro/alt-ergo/blob/next/publications/Alt-Ergo-2.2--SMT-Workshop-2018.pdf},
  address = {Oxford, UK}
}
@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{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}
}
@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,
  title = {VSTTE 2016},
  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,
  series = {Lecture Notes in Computer Science},
  volume = {9690},
  publisher = {Springer}
}
@inproceedings{chargueraud-pottier-15,
  author = {Arthur Chargu\'eraud and Fran\c{c}ois Pottier},
  title = {Machine-Checked Verification of the Correctness and
                 Amortized Complexity of an Efficient Union-Find
                 Implementation},
  booktitle = {Proceedings of the 6th Conference on Interactive
                 Theorem Proving (ITP 2015)},
  month = aug,
  year = {2015},
  volume = {9236},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  pages = {137--153},
  url = {http://gallium.inria.fr/~fpottier/publis/chargueraud-pottier-uf.pdf}
}
@inproceedings{chargueraud-pottier-slro-16,
  author = {Arthur Chargu\'eraud and Fran\c{c}ois Pottier},
  title = {Temporary Read-Only Permissions for Separation Logic},
  booktitle = {Proceedings of the European Symposium on Programming
                 (ESOP 2017)},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  editor = {Hongseok Yang},
  month = apr,
  year = {2017},
  url = {http://gallium.inria.fr/~fpottier/publis/chargueraud-pottier-slro.pdf}
}
@inproceedings{pottier-cpp-17,
  author = {Fran\c{c}ois Pottier},
  title = {Verifying a hash table and its iterators in
                 higher-order separation logic},
  booktitle = {Proceedings of the 6th ACM SIGPLAN Conference on
                 Certified Programs and Proofs (CPP 2017)},
  month = jan,
  year = {2017},
  pages = {3--16},
  url = {http://gallium.inria.fr/~fpottier/publis/fpottier-hashtable.pdf}
}
@article{chargueraud-pottier-uf-sltc-17,
  author = {Arthur Chargu\'eraud and Fran\c{c}ois Pottier},
  title = {Verifying the Correctness and Amortized Complexity of
                 a Union-Find Implementation in Separation Logic with
                 Time Credits},
  journal = {Journal of Automated Reasoning},
  month = sep,
  year = 2017,
  url = {http://gallium.inria.fr/~fpottier/publis/chargueraud-pottier-uf-sltc.pdf},
  hal = {https://hal.inria.fr/hal-01652785}
}
@misc{cfpp17,
  topics = {team},
  author = {Arthur Chargu\'eraud and Jean-Christophe Filli{\^a}tre and
                  M{\'a}rio Pereira and Fran\c{c}ois Pottier},
  title = {{VOCAL} -- {A} {V}erified {OC}aml {L}ibrary},
  howpublished = {ML Family Workshop},
  month = {September},
  year = {2017},
  hal = {https://hal.inria.fr/hal-01561094}
}
@inproceedings{pereira17jfla,
  topics = {team},
  title = {{D{\'e}fonctionnaliser pour prouver}},
  author = {Pereira, M{\'a}rio},
  hal = {https://hal.inria.fr/hal-01378068},
  crossref = {jfla17}
}
@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}
}
@unpublished{boulme:hal-01558252,
  title = {{Toward Certification for Free!}},
  author = {Boulm{\'e}, Sylvain and Mar{\'e}chal, Alexandre},
  url = {https://hal.archives-ouvertes.fr/hal-01558252},
  note = {working paper or preprint},
  year = {2017},
  month = jul,
  keywords = { Linear Programming ; Coq ; Type theory ; Abstract Domain of Polyhedra ; Polymorphism ; Program verification ;  Parametricity ; CCS Concepts: $\bullet$Software and its engineering $\rightarrow$ Polymorphism ; $\bullet$Theory of computation $\rightarrow$ Program veriication ; Invariants ; $\bullet$Mathematics of computing $\rightarrow$ Solvers ; Additional Key Words and Phrases: Abstract Domain of Polyhedra ;  CCC},
  pdf = {https://hal.archives-ouvertes.fr/hal-01558252/file/PFS.pdf},
  hal_id = {hal-01558252},
  hal_version = {v2}
}
@inproceedings{chargueraud-ml-17,
  author = {Arthur Chargu\'eraud and Mike Rainey},
  title = {Efficient Representations for Large Dynamic Sequences in ML},
  booktitle = {ML Family Workshop},
  year = 2017,
  hal = {https://hal.inria.fr/hal-01669407}
}
@inproceedings{gueneau-chargueraud-pottier-esop-2018,
  author = {Arma\"el Gu\'eneau and Arthur Chargu\'eraud and Fran\c{c}ois
                 Pottier},
  title = {A Fistful of Dollars: Formalizing Asymptotic
                 Complexity Claims via Deductive Program Verification},
  booktitle = {Proceedings of the European Symposium on Programming
                 (ESOP 2018)},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  editor = {Amal Ahmed},
  month = apr,
  year = {2018},
  volume = {10801},
  pages = {533--560},
  url = {http://gallium.inria.fr/~agueneau/publis/gueneau-chargueraud-pottier-coq-bigO.pdf}
}
@article{clochard17jar,
  topics = {team},
  title = {The {Matrix} Reproved},
  author = {Clochard, Martin and Gondelman, L{\'e}on and Pereira, M{\'a}rio},
  hal = {https://hal.inria.fr/hal-01617437},
  journal = jar,
  pages = {365--383},
  volume = 60,
  number = 3,
  publisher = sv,
  year = 2018,
  doi = {10.1007/s10817-017-9436-2}
}
@inproceedings{fpds18jfla,
  topics = {team},
  crossref = {jfla18},
  title = {V{\'e}rification de programmes fortement imp{\'e}ratifs avec {W}hy3},
  author = {Jean-Christophe Filli{\^a}tre and M{\'a}rio Pereira and
  Sim{\~a}o Melo de Sousa},
  hal = {https://hal.inria.fr/hal-01649989},
  pdf = {https://hal.inria.fr/hal-01649989/file/main.pdf},
  hal_id = {hal-01649989},
  hal_version = {v2}
}
@proceedings{jfla18,
  topics = {team},
  title = {Vingt-neuvi\`emes Journ\'ees Francophones des Langages Applicatifs},
  booktitle = {Vingt-neuvi\`emes Journ{\'e}es Francophones des Langages Applicatifs},
  address = {Banyuls-sur-mer, France},
  year = 2018,
  month = jan,
  editor = {Boldo, Sylvie and Magaud, Nicolas},
  hal = {https://hal.inria.fr/hal-01707376}
}
@techreport{fgpps18,
  author = {Jean-Christophe Filli{\^a}tre and L{\'e}on Gondelman and
            Andrei Paskevich and M{\'a}rio Pereira and Sim{\~a}o Melo de Sousa},
  title = {A Toolchain to {P}roduce {C}orrect-by-{C}onstruction {OC}aml
           {P}rograms},
  hal = {https://hal.inria.fr/hal-01783851},
  pdf = {https://hal.inria.fr/hal-01783851/file/main.pdf},
  note = {\url{https://hal.inria.fr/hal-01783851}}
}
@inproceedings{gospelfm19,
  topics = {team},
  crossref = {fm19},
  author = {Arthur Chargu\'eraud and Jean-Christophe Filli\^atre and Cl\'audio Louren\c{c}o and M\'ario Pereira},
  title = {{GOSPEL} --- Providing {OCaml} with a Formal Specification Language},
  hal = {https://hal.inria.fr/hal-02157484}
}
@proceedings{fm19,
  title = {FM 2019 23rd International Symposium on Formal Methods},
  year = 2019,
  editor = {Annabelle McIver and Maurice ter Beek},
  month = {October}
}
@misc{vocal,
  author = {The VOCaL project},
  title = {The {VOCaL} Library},
  howpublished = {Open Source Software, with MIT license},
  year = 2018,
  note = {\url{https://github.com/vocal-project/vocal}}
}
@misc{tis-report-1,
  author = {TrustInSoft},
  title = {Report on the deployment of the {VOCaL} library in {TrustInSoft} Kernel},
  year = 2019,
  month = {May}
}

This file was generated by bibtex2html 1.99.