Suivre
Mário Pereira
Mário Pereira
Assistant Professor, NOVA School of Science and Technology
Adresse e-mail validée de fct.unl.pt - Page d'accueil
Titre
Citée par
Citée par
Année
A modular way to reason about iteration
JC Filliâtre, M Pereira
NASA Formal Methods Symposium, 322-336, 2016
242016
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
232019
Tools and techniques for the verification of modular stateful code
MJ Parreira Pereira
Université Paris-Saclay (ComUE), 2018
202018
The matrix reproved (verification pearl)
M Clochard, L Gondelman, M Pereira
Journal of Automated Reasoning 60, 365-383, 2018
132018
VOCAL–A Verified OCaml Library
A Charguéraud, JC Filliâtre, M Pereira, F Pottier
132017
Itérer avec confiance
JC Filliâtre, M Pereira
Journées Francophones des Langages Applicatifs, 2016
92016
Verifying reliable network components in a distributed separation logic with dependent separation protocols
L Gondelman, JK Hinrichsen, M Pereira, A Timany, L Birkedal
Proceedings of the ACM on Programming Languages 7 (ICFP), 847-877, 2023
82023
Cameleer: a Deductive Verification Tool for OCaml
M Pereira, A Ravara
International Conference on Computer-Aided Verification, 677-689, 2021
72021
Whylson: Proving your michelson smart contracts in why3
LPA da Horta, JS Reis, M Pereira, SM de Sousa
arXiv preprint arXiv:2005.14650, 2020
72020
A coordination-free, convergent, and safe replicated tree
S Nair, F Meirim, M Pereira, C Ferreira, M Shapiro
arXiv preprint arXiv:2103.04828, 2021
62021
Défonctionnaliser pour prouver
M Pereira
JFLA 2017-Vingt-huitième Journées Francophones des Langages Applicatifs, 2017
62017
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
42020
Liquid intersection types
MJP Pereira
PQDT-Global, 2014
42014
Desfuncionalizar para Provar
M Pereira
arXiv preprint arXiv:1905.08368, 2019
32019
Animated logic: correct functional conversion to conjunctive normal form
P Barroso, M Pereira, A Ravara
arXiv preprint arXiv:2003.05081, 2020
22020
A toolchain to produce verified OCaml libraries
JC Filliâtre, L Gondelman, C Lourenço, A Paskevich, M Pereira, ...
22020
A Toolchain to Produce Correct-by-Construction OCaml Programs
JC FilliÂtRe, L Gondelman, A Paskevich, M Pereira, SM de Sousa
Rapp. tech. artifact: https://www. lri. fr/~ mpereira/correct_ocaml. ova, 2018
22018
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
Verificação de Programas OCaml Imperativos de Ordem Superior, através de Desfuncionalização
T Soares, M Pereira
12º Simpósio em Informática (INForum 2021), 2021
12021
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
12019
Le système ne peut pas réaliser cette opération maintenant. Veuillez réessayer plus tard.
Articles 1–20