| 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 | 33 | 2019 |
| A modular way to reason about iteration JC Filliâtre, M Pereira NASA Formal Methods Symposium, 322-336, 2016 | 25 | 2016 |
| Cameleer: a Deductive Verification Tool for OCaml M Pereira, A Ravara International Conference on Computer-Aided Verification, 677-689, 2021 | 21 | 2021 |
| Tools and techniques for the verification of modular stateful code MJP Pereira Université Paris Saclay (COmUE), 2018 | 21 | 2018 |
| VOCAL–A Verified OCaml Library A Charguéraud, JC Filliâtre, M Pereira, F Pottier | 15 | 2017 |
| 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 | 13 | 2023 |
| The matrix reproved (verification pearl) M Clochard, L Gondelman, M Pereira Journal of Automated Reasoning 60, 365-383, 2018 | 13 | 2018 |
| Itérer avec confiance JC Filliâtre, M Pereira Journées Francophones des Langages Applicatifs, 2016 | 9 | 2016 |
| Whylson: Proving your michelson smart contracts in why3 LPA da Horta, JS Reis, M Pereira, SM de Sousa arXiv preprint arXiv:2005.14650, 2020 | 8 | 2020 |
| 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 | 7 | 2020 |
| A coordination-free, convergent, and safe replicated tree S Nair, F Meirim, M Pereira, C Ferreira, M Shapiro arXiv preprint arXiv:2103.04828, 2021 | 6 | 2021 |
| Défonctionnaliser pour prouver M Pereira JFLA 2017-Vingt-huitième Journées Francophones des Langages Applicatifs, 2017 | 6 | 2017 |
| Liquid intersection types MJP Pereira PQDT-Global, 2014 | 4 | 2014 |
| A toolchain to produce verified OCaml libraries JC Filliâtre, L Gondelman, C Lourenço, A Paskevich, M Pereira, ... | 3 | 2020 |
| Desfuncionalizar para Provar M Pereira arXiv preprint arXiv:1905.08368, 2019 | 3 | 2019 |
| 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 | 2 | 2024 |
| A Framework for the Automated Verification of Algebraic Effects and Handlers (extended version) T Soares, M Pereira arXiv preprint arXiv:2302.01265, 2023 | 2 | 2023 |
| 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 | 2 | 2021 |
| Animated logic: correct functional conversion to conjunctive normal form P Barroso, M Pereira, A Ravara arXiv preprint arXiv:2003.05081, 2020 | 2 | 2020 |
| 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 | 2 | 2018 |
Jean-Christophe FilliâtreCNRSVerified email at lri.fr
