Seguir
Mário Pereira
Mário Pereira
Assistant Professor, NOVA School of Science and Technology
Email confirmado em fct.unl.pt - Página inicial
Título
Citado por
Citado por
Ano
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
372019
A modular way to reason about iteration
JC Filliâtre, M Pereira
NASA Formal Methods Symposium, 322-336, 2016
252016
Cameleer: a Deductive Verification Tool for OCaml
M Pereira, A Ravara
International Conference on Computer-Aided Verification, 677-689, 2021
242021
Tools and techniques for the verification of modular stateful code
MJP Pereira
Université Paris Saclay (COmUE), 2018
212018
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
172023
VOCAL–A Verified OCaml Library
A Charguéraud, JC Filliâtre, M Pereira, F Pottier
152017
The matrix reproved (verification pearl)
M Clochard, L Gondelman, M Pereira
Journal of Automated Reasoning 60, 365-383, 2018
132018
Itérer avec confiance
JC Filliâtre, M Pereira
Journées Francophones des Langages Applicatifs, 2016
102016
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
72020
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
Liquid intersection types
MJP Pereira
PQDT-Global, 2014
42014
A toolchain to produce verified OCaml libraries
JC Filliâtre, L Gondelman, C Lourenço, A Paskevich, M Pereira, ...
32020
Desfuncionalizar para Provar
M Pereira
arXiv preprint arXiv:1905.08368, 2019
32019
Static and dynamic verification of OCAML programs: the gospel ecosystem
TL Soares, I Chirica, M Pereira
International Symposium on Leveraging Applications of Formal Methods, 247-265, 2024
22024
A Framework for the Automated Verification of Algebraic Effects and Handlers (extended version)
T Soares, M Pereira
arXiv preprint arXiv:2302.01265, 2023
22023
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
22021
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 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
O sistema não pode efectuar a operação agora. Tente mais tarde.
Artigos 1–20