pereira.bib
@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc pereira.cite -ob pereira.bib -c 'author : "Mário Pereira\|Pereira, Mário"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}
@inproceedings{DBLP:conf/cav/PereiraR20,
author = {M{\'{a}}rio Pereira and
Ant{\'{o}}nio Ravara},
editor = {Alexandra Silva and
K. Rustan M. Leino},
title = {{Cameleer: {A} Deductive Verification Tool for OCaml}},
booktitle = {Computer Aided Verification - 33rd International Conference, {CAV}
2021, Virtual Event, July 20-23, 2021, Proceedings, Part {II}},
series = {Lecture Notes in Computer Science},
volume = {12760},
pages = {677--689},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-81688-9_31},
doi = {10.1007/978-3-030-81688-9_31},
timestamp = {Wed, 21 Jul 2021 14:40:49 +0200},
biburl = {https://dblp.org/rec/conf/cav/PereiraR20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{filliatre12inforum,
author = {M\'ario Pereira and Jean-Christophe Filli\^atre and
Sim{\~a}o Melo de Sousa},
title = {{ARMY}: a Deductive Verification Platform for {ARM} Programs Using {Why3}},
month = {September},
year = 2012,
type_publi = {icolcomlec},
x-international-audience = {yes},
x-proceedings = {no},
x-equipes = {demons PROVAL ext},
x-support = {rapport},
x-cle-support = {INFORUM},
x-type = {article},
topics = {team},
keywords = {Why3},
abstract = {Unstructured (low-level) programs tend to be challenging
to prove correct, since the control flow is
arbitrary complex and there are no obvious points in
the code where to insert logical assertions. In this
paper, we present a system to formally verify ARM
programs, based on a flow sequentialization
methodology and a formalized ARM semantics. This
system, built upon the why3 verification platform,
takes an annotated ARM program, turns it into a set
of purely sequential flow programs, translates these
programs' instructions into the corresponding
formalized opcodes and finally calls the Why3 VCGen
to generate the verification conditions that can
then be discharged by provers. A prototype has been
implemented and used to verify several programming
examples.},
booktitle = {INForum 2012},
url = {http://inforum.org.pt/INForum2012/docs/20120013.pdf}
}
@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}
}
@inproceedings{pereira17jfla,
topics = {team},
title = {{D{\'e}fonctionnaliser pour prouver}},
author = {Pereira, M{\'a}rio},
hal = {https://hal.inria.fr/hal-01378068},
crossref = {jfla17}
}
@misc{cfpp17,
topics = {team},
author = {Arthur Chargu{\'e}raud 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}
}
@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 = {Journal of Automated Reasoning},
pages = {365--383},
volume = 60,
number = 3,
publisher = {Springer},
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}
}
@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 = {artifact: \url{https://www.lri.fr/~mpereira/correct_ocaml.ova}},
year = {2018}
}
@phdthesis{pereira18phd,
topics = {team},
title = {Tools and Techniques for the Verification of Modular Stateful Code},
author = {Pereira, M{\'a}rio},
school = {Universit{\'e} Paris-Saclay},
year = 2018,
month = dec,
type = {Th{\`e}se de Doctorat}
}
@inproceedings{gospelfm19,
topics = {team},
crossref = {fm19},
author = {Arthur Chargu\'eraud and Jean-Christophe Filli\^atre and Cl\'audio Belo 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{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{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{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}
}
@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}
}
@proceedings{fm19,
title = {FM 2019 23rd International Symposium on Formal Methods},
booktitle = {FM 2019 23rd International Symposium on Formal Methods},
month = oct,
year = 2019,
address = {Porto, Portugal},
editor = {Annabelle McIver and Maurice ter Beek}
}