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
152016
Itérer avec confiance
JC Filliâtre, M Pereira
92016
Tools and Techniques for the Verification of Modular Stateful Code
MJ Parreira Pereira
Paris Saclay, 2018
8*2018
The Matrix Reproved (Verification Pearl)
M Clochard, L Gondelman, M Pereira
Journal of Automated Reasoning 60 (3), 365-383, 2018
82018
VOCAL–A Verified OCAml Library
A Charguéraud, JC Filliâtre, M Pereira, F Pottier
72017
Défonctionnaliser pour prouver
M Pereira
42017
Liquid intersection types
M Pereira, S Alves, M Florido
arXiv preprint arXiv:1503.04908, 2015
32015
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
22019
Desfuncionalizar para Provar
M Pereira
arXiv preprint arXiv:1905.08368, 2019
22019
A Toolchain to Produce Correct-by-Construction OCaml Programs
JC Filliâtre, L Gondelman, A Paskevich, M Pereira, SM de Sousa
12018
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
12014
Liquid Types Revisited
M Pereira, S Alves, M Florido
The 20th TYPES Meeting, Paris, France, 2014
12014
WhylSon: Proving your Michelson Smart Contracts in Why3
LPA da Horta, JS Reis, M Pereira, SM de Sousa
arXiv preprint arXiv:2005.14650, 2020
2020
WhylSon: Proving your Michelson Smart Contracts in Why3
LP Arrojado da Horta, J Santos Reis, M Pereira, S Melo de Sousa
arXiv, arXiv: 2005.14650, 2020
2020
Animated Logic: Correct Functional Conversion to Conjunctive Normal Form
P Barroso, M Pereira, A Ravara
arXiv preprint arXiv:2003.05081, 2020
2020
A Toolchain to Produce Verified OCaml Libraries
JC Filliâtre, L Gondelman, C Lourenço, A Paskevich, M Pereira, ...
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
Vérification de programmes OCaml fortement impératifs avec Why3
JC Filliâtre, M Pereira, SM de Sousa
2018
Producing All Ideals of a Forest, Formally (Verification Pearl)
JC Filliâtre, M Pereira
Working Conference on Verified Software: Theories, Tools, and Experiments, 46-55, 2016
2016
Liquid Intersection Types
MPSAM Florido
2014
The system can't perform the operation now. Try again later.
Articles 1–20