Hello and welcome to my small corner in the web! :D

I am a PhD student at LRI, Université Paris-Sud. My supervisor is Jean-Christophe Filliâtre and I am conducting my research in the VALS team.


I'm doing research in Deductive Software Verification. I'm an enthusiast of the Why3 tool and more generally of the auto-active approach to program verification. In the scope of my PhD, I'm studying ways to extend Why3 to support higher-order (effectful) programming.

From 2012 to 2014 I was a master student at the Computer Science Department at University of Oporto. During my master thesis I studied refinement type systems, particularly Liquid Types, and intersection types. I designed and implemented a new type system combining refinement predicates and the accuracy offered by intersection types discipline, the Liquid Intersection Type system. This work is described in my master thesis and in this paper. My supervisors were Sandra Alves and Mario Florido.

From 2009 to 2012 I was an undergraduate student at the Computer Engineering Department of University of Beira Interior. As my bacherol final project, I developed a platform to specify and prove programs written in ARM Assembly language. Take a look at this paper if you got interested. My supervisor was Simao Melo de Sousa.

Program verification

Verifying programs has been a constant in my academic life. I made my first experiences around program proving (using the Why3 tool) in 2011, at the age of 20. It comes with no surprise that I am still doing verification these days and that this ended up being my PhD research area.

I gather in this section a selected set of documents and links about the activity of program verification. I also publish examples that I had fun proving myself.

What is program verification?

Who better than the masters to explain this amazing subject? Let them speak:

My own "pearls"


I really love computer programming, especially functional programming. I am a big fan of the OCaml language