Mário Pereira

Mário Pereira is an Assistant Professor at NOVA School of Science and Technology, NOVA University of Lisbon. He is also an Integrated Member of NOVA LINCS (NOVA Laboratory of Computer Science and Informatics).

Dr. Pereira's research focuses on Deductive Software Verification, with particular expertise in program verification techniques and tools. His work centers on the deductive verification of OCaml programs, where he has developed tools and techniques as part of his Marie Sklodowska-Curie project "Cameleer." He is an enthusiast of the Why3 verification tool and the auto-active approach to program verification. His research spans formal methods, type systems (including refinement types and intersection types), and the development of verified software libraries.

Among his notable achievements, Dr. Pereira was a Marie Sklodowska-Curie Fellow from June 2020 to May 2022, working on the Cameleer project at NOVA-LINCS. This prestigious fellowship supported his research in developing tools for the deductive verification of OCaml programs.

Dr. Pereira has extensive teaching experience, having served as a teaching assistant since 2016. At FCT/Universidade Nova de Lisboa since 2020, he has taught courses including Theory of Computation and Analysis and Design of Algorithms. Previously, he taught at École Polytechnique in France, where he assisted in courses such as Introduction to Computer Science, Programming and Algorithms Basis, Advanced Programming, and Compilers.

As an active member of the research community, Dr. Pereira contributes to several open-source software projects related to program verification, including Cameleer (a deductive verification tool for OCaml), Why3 (a software verification framework), OCamlGraph (a graph library for OCaml), and VOCaL (the Verified OCaml Library). He maintains an active GitHub presence under the username mariojppereira.