I am a research engineer in the Toccata@INRIA Saclay and VALS@LRI teams. My main professional interests are in program verification and functional programming. I am currently working on the implementation of new functionalities for the Why3 deductive verification tool and on the design and implementation of a specification language for OCaml interfaces in the context of the VOCaL Project.
I finished my PhD (title: Single-assignment Program Verification) in 2018 at Universidade do Minho & HASLab / INESC TEC, under the supervision of Jorge Sousa Pinto. During this period I did an internship at the National Institute of Informatics (Japan) under the supervision of Shin Nakajima and I was a visiting researcher in the Why3 team for half a year.
I completed my Master degree (2013) in Software Engineering at the University of Minho, where I studied mainly formal methods and distributed systems. My thesis (title: A Bounded Model Checker for SPARK Programs), supervised by Jorge Sousa Pinto and Maria João Frade, focused on formal verification of Ada/SPARK programs. I graduated (2011) in Computer Science at the Universidade do Minho, having attended one year at the University of Groningen, Netherlands, under the Erasmus Program.
Address: LRI - Bâtiment 650, Université Paris-Sud, 91405 ORSAY cedex, FRANCE