Takip et
Mário Pereira
Mário Pereira
Assistant Professor, NOVA School of Science and Technology
fct.unl.pt üzerinde doğrulanmış e-posta adresine sahip - Ana Sayfa
Başlık
Alıntı yapanlar
Alıntı yapanlar
Yıl
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
362019
Cameleer: a Deductive Verification Tool for OCaml
M Pereira, A Ravara
International Conference on Computer-Aided Verification, 677-689, 2021
252021
A modular way to reason about iteration
JC Filliâtre, M Pereira
NASA Formal Methods Symposium, 322-336, 2016
252016
Tools and techniques for the verification of modular stateful code
MJP Pereira
Université Paris Saclay (COmUE), 2018
192018
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
152023
The matrix reproved (verification pearl)
M Clochard, L Gondelman, M Pereira
Journal of Automated Reasoning 60, 365-383, 2018
152018
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
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
52017
Liquid intersection types
MJP Pereira
PQDT-Global, 2014
42014
A framework for the automated verification of algebraic effects and handlers (extended version)
T Soares, M Pereira
arXiv preprint arXiv:2302.01265, 2023
32023
Animated logic: correct functional conversion to conjunctive normal form
P Barroso, M Pereira, A Ravara
arXiv preprint arXiv:2003.05081, 2020
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
Practical Deductive Verification of OCaml Programs
M Pereira
International Symposium on Formal Methods, 518-542, 2024
22024
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
Sistem, işlemi şu anda gerçekleştiremiyor. Daha sonra yeniden deneyin.
Makaleler 1–20