Mário Pereira

Mário Pereira is an Assistant Professor at the Computer Science Department of Nova School of Science and Technology, as well as an Integrated Member of the NOVA LINCS research lab. His main research interests lie in the fields of Deductive Software Verification and Functional Programming, with a particular focus on the formal verification of OCaml programs. Before joining FCT/UNL as a faculty member, Mário Pereira was a Marie-Sklodowska-Curie fellow and Assistant Researcher at NOVA LINCS. He was awarded this fellowship by the European Commission due to his experience and expertise in deductive software verification. His project "Cameleer - Principles and Methods to Verify OCaml Programs" was awarded a 98.4% grad (top 10%) in a highly-competitive selection process. Mário is a PhD in Computer Science from Université Paris-Saclay. He successfully defended his PhD thesis "Tools and Techniques for the Verification of Modular Stateful Code" under the pervision of Jean-Christophe Filliâtre, senior researcher of CNRS (the French national institute for public research) and the original author of the Why3 framework. Prior to his PhD, Mário was an MSc student at Faculty of Sciences of Oporto, where he developed a new calculus combining refinement and intersection types. He was advised by Mário Florido and Sandra Alves. Even before, during his BSc, he developed with Simão Melo de Sousa a deductive framework for the WCET analysis of machine-level code. Mário is the architect and lead developer of Cameleer, a new tool for the deductive verification of OCaml code. He is also one of the authors of GOSPEL, the Generic Ocaml SPEcification Language. He has recently published his work on top international venues (e.g., International Conference on Computer Aided Verification, International Symposium on Formal Methods), as well as prestigious Computer Science journals (e.g., Journal of Automated Reasoning). He is a member of the SMARTY project (funded by FCT, 2022.09138.PTDC), where he leads the work package on formalization of smart contracts virtual machines. He was a member of the LEAFS project, a research project financed by the OCaml Foundation, where he led the task on syntactic programs transformation. He was a member of the FRESCO and FACTOR projects (funded by the Tezos Foundations), the PRECISE project (funded by FCT, PTDC/CCIINF/32081/2017). During his PhD, Mário was a member of the VOCAL (a Verified OCAml Library) research project (funded by ANR, 15-CE25-0008, the French national research agency). Mário has already supervised seven master thesis in computer science from FCT/NOVA and six bachelor thesis (one from École Normale Supérieure de Lyon, two from University of Beira Interior, and three from FCT/NOVA). He is currently supervising two PhD students and two master students.