Mário Pereira
Mário Pereira
Marie Curie Fellow, NOVA-LINCS
Verified email at fct.unl.pt - Homepage
Title
Cited by
Cited by
Year
A modular way to reason about iteration
JC Filliâtre, M Pereira
NASA Formal Methods Symposium, 322-336, 2016
142016
Tools and Techniques for the Verification of Modular Stateful Code
MJ Parreira Pereira
Université Paris-Saclay (ComUE), 2018
132018
The matrix reproved (verification pearl)
M Clochard, L Gondelman, M Pereira
Journal of Automated Reasoning 60 (3), 365-383, 2018
102018
GOSPEL—Providing OCaml with a Formal Specification Language
A Charguéraud, JC Filliâtre, C Lourenço, M Pereira
International Symposium on Formal Methods, 484-501, 2019
82019
VOCAL–A Verified OCaml Library
A Charguéraud, JC Filliâtre, M Pereira, F Pottier
82017
Itérer avec confiance
JC Filliâtre, M Pereira
Journées Francophones des Langages Applicatifs, 2016
72016
Défonctionnaliser pour prouver
M Pereira
JFLA 2017-Vingt-huitième Journées Francophones des Langages Applicatifs, 2017
52017
A coordination-free, convergent, and safe replicated tree
S Nair, F Meirim, M Pereira, C Ferreira, M Shapiro
arXiv preprint arXiv:2103.04828, 2021
42021
Desfuncionalizar para Provar
M Pereira
arXiv preprint arXiv:1905.08368, 2019
32019
Liquid intersection types
M Pereira, S Alves, M Florido
arXiv preprint arXiv:1503.04908, 2015
32015
WhylSon: Proving your Michelson Smart Contracts in Why3
LPA da Horta, JS Reis, M Pereira, SM de Sousa
arXiv preprint arXiv:2005.14650, 2020
22020
Complexity checking of ARM programs, by deduction
M Pereira, SM de Sousa
Proceedings of the 29th Annual ACM Symposium on Applied Computing, 1309-1314, 2014
22014
A tool for proving Michelson Smart Contracts in WHY3*
LPA da Horta, JS Reis, SM de Sousa, M Pereira
2020 IEEE International Conference on Blockchain (Blockchain), 409-414, 2020
12020
Animated Logic: Correct Functional Conversion to Conjunctive Normal Form
P Barroso, M Pereira, A Ravara
arXiv preprint arXiv:2003.05081, 2020
12020
A Toolchain to Produce Verified OCaml Libraries
JC Filliâtre, L Gondelman, C Lourenço, A Paskevich, M Pereira, ...
12020
Liquid Types Revisited
M Pereira, S Alves, M Florido
The 20th TYPES Meeting, Paris, France, 2014
12014
Cameleer: a Deductive Verification Tool for OCaml
M Pereira, A Ravara
International Conference on Computer-Aided Verification, 677-689, 2021
2021
Cameleer: a Deductive Verification Tool for OCaml (extended version)
M Pereira, A Ravara
32 ème Journées Francophones des Langages Applicatifs, 2021
2021
CISE3: Verifying Weakly Consistent Applications with Why3
F Meirim, M Pereira, C Ferreira
arXiv preprint arXiv:2010.06622, 2020
2020
CISE3: Verifica\c {c}\~ ao de aplica\c {c}\~ oes com consist\^ encia fraca em Why3
F Meirim, M Pereira, C Ferreira
arXiv preprint arXiv:1909.03721, 2019
2019
The system can't perform the operation now. Try again later.
Articles 1–20