Mário Pereira

Publication Activity (10 Years)

Years Active: 2014-2024
Publications (10 Years): 23

Top Topics

Conjunctive Normal Form

Top Venues

Proc. ACM Program. Lang.

Publications

Tiago Lopes Soares, Ion Chirica, Mário Pereira
Static and Dynamic Verification of OCaml Programs: The Gospel Ecosystem (Extended Version). CoRR (2024)
Mário Pereira
The Theory and Practice of Deductive Verification of OCaml Programs. CoRR (2024)
Léon Gondelman, Jonas Kastberg Hinrichsen, Mário Pereira, Amin Timany, Lars Birkedal
Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols. Proc. ACM Program. Lang. 7 (ICFP) (2023)
Tiago Soares, Mário Pereira
A Framework for the Automated Verification of Algebraic Effects and Handlers (extended version). CoRR (2023)
Daniel Castanho, Mário Pereira
Auto-active Verification of Graph Algorithms, Written in OCaml. CoRR (2022)
Pedro Barroso, Mário Pereira, António Ravara
Leroy and Blazy were right: their memory model soundness proof is automatable (Extended Version). CoRR (2022)
Pedro Barroso, Mário Pereira, António Ravara
Leroy and Blazy Were Right: Their Memory Model Soundness Proof is Automatable. VSTTE (2022)
Sreeja Nair, Filipe Meirim, Mário Pereira, Carla Ferreira, Marc Shapiro
A coordination-free, convergent, and safe replicated tree. CoRR (2021)
Mário Pereira, António Ravara
Cameleer: a Deductive Verification Tool for OCaml. CoRR (2021)
Mário Pereira, António Ravara
Cameleer: A Deductive Verification Tool for OCaml. CAV (2) (2021)
Pedro Barroso, Mário Pereira, António Ravara
Animated Logic: Correct Functional Conversion to Conjunctive Normal Form. PAAR+SC²@IJCAR (2020)
Pedro Barroso, Mário Pereira, António Ravara
Animated Logic: Correct Functional Conversion to Conjunctive Normal Form. CoRR (2020)
Filipe Meirim, Mário Pereira, Carla Ferreira
CISE3: Verifying Weakly Consistent Applications with Why3. CoRR (2020)
Luís Pedro Arrojado da Horta, João Santos Reis, Simão Melo de Sousa, Mário Pereira
. Blockchain (2020)
Luís Pedro Arrojado da Horta, João Santos Reis, Mário Pereira, Simão Melo de Sousa
WhylSon: Proving your Michelson Smart Contracts in Why3. CoRR (2020)
Arthur Charguéraud, Jean-Christophe Filliâtre, Cláudio Lourenço, Mário Pereira
GOSPEL - Providing OCaml with a Formal Specification Language. FM (2019)
Marta Pinto, Mário Pereira, Diana Raposo, Marco Simões, Miguel Castelo-Branco
GameAAL - an AAL solution based on Gamification and Machine Learning Techniques. CIBCB (2019)
Mário Pereira
Desfuncionalizar para Provar. CoRR (2019)
Filipe Meirim, Mário Pereira, Carla Ferreira
CISE3: Verificação de aplicações com consistência fraca em Why3. CoRR (2019)
Martin Clochard, Léon Gondelman, Mário Pereira
The Matrix Reproved (Verification Pearl). J. Autom. Reason. 60 (3) (2018)
Martin Clochard, Léon Gondelman, Mário Pereira
The Matrix Reproved (Verification Pearl). VSTTE (2016)
Jean-Christophe Filliâtre, Mário Pereira
A Modular Way to Reason About Iteration. NFM (2016)
Jean-Christophe Filliâtre, Mário Pereira
Producing All Ideals of a Forest, Formally (Verification Pearl). VSTTE (2016)
Filipe Teixeira, José Santos, Luís M. Pessoa, Mário Pereira, Rui Campos, Manuel Ricardo
Evaluation of Underwater IEEE 802.11 Networks at VHF and UHF Frequency Bands using Software Defined Radios. WUWNet (2015)
Mário Pereira, Sandra Alves, Mário Florido
Liquid Intersection Types. ITRS (2014)
Mário Pereira, Simão Melo de Sousa
Complexity checking of ARM programs, by deduction. SAC (2014)