pereira.bib

@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{pereira14sac,
  author = {Pereira, M\'{a}rio and de Sousa, Sim\~{a}o Melo},
  title = {Complexity Checking of ARM Programs, by Deduction},
  booktitle = {Proceedings of the 29th Annual ACM Symposium on Applied Computing},
  series = {SAC '14},
  year = {2014},
  isbn = {978-1-4503-2469-4},
  location = {Gyeongju, Republic of Korea},
  pages = {1309--1314},
  numpages = {6},
  url = {http://doi.acm.org/10.1145/2554850.2555012},
  doi = {10.1145/2554850.2555012},
  acmid = {2555012},
  publisher = {ACM},
  address = {New York, NY, USA},
  keywords = {ARM, complexity checking, deductive software verification, hoare
                  logic, unstructured control flow graph, why3}
}
@article{pereira14itrs,
  author = {Pereira, Mário and Alves, Sandra and Florido, Mário},
  title = {Liquid Intersection Types},
  journal = {Electronic Proceedings in Theoretical Computer Science},
  volume = {177},
  pages = {24--42},
  year = {2015},
  month = {mar},
  url = {http://dx.doi.org/10.4204/eptcs.177.3},
  doi = {10.4204/eptcs.177.3}
}
@inproceedings{pereira16jfla,
  x-cle-support = {JFLA},
  x-support = {actes_aux},
  x-type = {article},
  x-proceedings = {yes},
  x-editorial-board = {yes},
  x-international-audience = {no},
  address = {Saint-Malo, France},
  month = jan,
  booktitle = {Vingt-septi\`emes Journ\'ees Francophones des Langages Applicatifs},
  year = 2016,
  topics = {team},
  author = {Jean-Christophe Filli\^atre and M\'ario Pereira},
  title = {It\'erer avec confiance},
  hal = {https://hal.inria.fr/hal-01240891}
}
@inproceedings{pereira16nfm,
  publisher = {Springer},
  volume = {9690},
  series = {Lecture Notes in Computer Science},
  editor = {Rayadurgam, Sanjai and Tkachuk, Oksana},
  month = jun,
  year = 2016,
  audience = {internationale},
  address = {Minneapolis, MN, USA},
  booktitle = {8th NASA Formal Methods Symposium},
  topics = {team},
  author = {Jean-Christophe Filli\^atre and M\'ario Pereira},
  title = {A Modular Way to Reason About Iteration},
  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,
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  editor = {Sandrine Blazy and Marsha Chechik},
  x-cle-support = {VSTTE},
  x-support = {actes},
  x-type = {article},
  x-proceedings = {yes},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  address = {Toronto, Canada},
  year = 2016,
  month = jul,
  booktitle = {8th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE)},
  topics = {team},
  author = {Jean-Christophe Filli\^atre and M\'ario Pereira},
  title = {Producing All Ideals of a Forest, Formally (Verification Pearl)},
  hal = {https://hal.inria.fr/hal-01316859}
}
@inproceedings{clochard16,
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  editor = {Sandrine Blazy and Marsha Chechik},
  x-cle-support = {VSTTE},
  x-support = {actes},
  x-type = {article},
  x-proceedings = {yes},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  address = {Toronto, Canada},
  year = 2016,
  month = jul,
  booktitle = {8th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE)},
  topics = {team},
  author = {Martin Clochard and L\'eon Gondelman and M\'ario Pereira},
  title = {The {Matrix} Reproved},
  hal = {https://hal.inria.fr/hal-01316902}
}
@inproceedings{pereira17jfla,
  x-cle-support = {JFLA},
  x-support = {actes_aux},
  x-type = {article},
  x-proceedings = {yes},
  x-editorial-board = {yes},
  x-international-audience = {no},
  address = {Gourette, France},
  month = jan,
  booktitle = {Vingt-huiti\`emes Journ\'ees Francophones des Langages Applicatifs},
  year = 2017,
  editor = {Boldo, Sylvie and Signoles, Julien},
  topics = {team},
  title = {{D{\'e}fonctionnaliser pour prouver}},
  author = {Pereira, M{\'a}rio},
  hal = {https://hal.inria.fr/hal-01378068}
}
@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,
  editor = {Boldo, Sylvie and Magaud, Nicolas},
  month = jan,
  year = 2018,
  address = {Banyuls-sur-mer, France},
  booktitle = {Vingt-neuvi\`emes Journ{\'e}es Francophones des Langages Applicatifs},
  topics = {team},
  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},
  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},
  note = {artifact: \url{https://www.lri.fr/~mpereira/correct_ocaml.ova}},
  year = {2018}
}
@phdthesis{parreirapereira:tel-01980343,
  title = {{Tools and Techniques for the Verification of Modular Stateful Code}},
  author = {Parreira Pereira, M{\'a}rio Jos{\'e}},
  url = {https://tel.archives-ouvertes.fr/tel-01980343},
  number = {2018SACLS605},
  school = {{Universit{\'e} Paris Saclay (COmUE)}},
  year = {2018},
  month = dec,
  keywords = {Modularity ; OCaml ; OCaml library ; Efects ; Why3 ; Deductive verification ; Modulaire ; OCaml ; V{\'e}rification d{\'e}ductive ; Why3 ; Effets ; Biblioth{\`e}que OCaml},
  type = {Theses},
  hal_id = {tel-01980343},
  hal_version = {v1}
}
@inproceedings{gospelfm19,
  editor = {Annabelle McIver and Maurice ter Beek},
  address = {Porto, Portugal},
  year = 2019,
  month = oct,
  booktitle = {FM 2019 23rd International Symposium on Formal Methods},
  topics = {team},
  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}},
  url = {https://hal.inria.fr/hal-02157484}
}
@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{soares21inforum,
  author = {Tiago Soares and M\'ario Pereira},
  title = {{Verifica\c{c}\~ao de Programas OCaml Imperativos de
Ordem Superior, atrav\'es de Desfuncionaliza\c{c}\~ao}},
  month = {September},
  year = 2021,
  type_publi = {icolcomlec},
  booktitle = {INForum 2021},
  url = {INForum_2020_paper_45.pdf}
}
@inproceedings{roxo19inforum,
  author = {Tiago Roxo and M\'ario Pereira and Sim{\~a}o Melo de Sousa},
  title = {{Programa\c{c}\~ao funcional com estilo e sem custo: Transforma\c{c}\~ao CPS \`a la carte}},
  month = {September},
  year = 2019,
  type_publi = {icolcomlec},
  booktitle = {INForum 2019},
  url = {INForum_2019_paper_4.pdf}
}
@inproceedings{barroso19inforum,
  author = {Pedro Barroso and M\'ario Pereira and Ant\'onio Ravara},
  title = {{L\'ogica Animada: convers\~ao funcional correta para forma normal conjuntiva}},
  month = {September},
  year = 2019,
  type_publi = {icolcomlec},
  booktitle = {INForum 2019},
  url = {INForum_2019_paper_6.pdf}
}
@inproceedings{meirim19inforum,
  author = {Filipe Meirim and M\'ario Pereira and Carla Ferreira},
  title = {{CISE3: Verifica\c{c}\~ao de aplica\c{c}\~oes com consist\^encia fraca em Why3}},
  month = {September},
  year = 2019,
  type_publi = {icolcomlec},
  booktitle = {INForum 2019},
  url = {INForum_2019_paper_8.pdf}
}
@inproceedings{horta19inforum,
  author = {Lu\'is Pedro Arrojado Horta and M\'ario Pereira and Sim{\~a}o Melo
                  de Sousa},
  title = {{Sem\^antica Operacional Execut\'avel para Michelson em Why3}},
  month = {September},
  year = 2019,
  type_publi = {icolcomlec},
  booktitle = {INForum 2019},
  url = {INForum_2019_paper_112.pdf}
}
@inproceedings{pereira19inforum,
  author = {M\'ario Pereira},
  title = {{Desfuncionalizar para Provar}},
  month = {September},
  year = 2019,
  type_publi = {icolcomlec},
  booktitle = {INForum 2019},
  url = {INForum_2019_paper_114.pdf}
}
@inproceedings{santos19inforum,
  author = {\'Alvaro Santos and M\'ario Pereira and Jo{\~a}o Leit{\~a}o and
                  Jo{\~a}o Costa Seco},
  title = {{Regent: Uma Arquitectura para a Evolu\c{c}\~ao de
                  Micro-Servi\c{c}os}},
  month = {September},
  year = 2019,
  type_publi = {icolcomlec},
  booktitle = {INForum 2019},
  url = {INForum_2019_paper_125.pdf}
}

This file was generated by bibtex2html 1.99.