About model and code verification

I will use this colloquium to present what I have been doing and learning during these three initial months at FMT. You will see that there is more learning than doing, this may hopefully have to do with me jumping from my former topic: Stochastic Automata for model checking, to my current topic which is static verification of code using VerCors. I will start showing you a little bit about how VerCors works, thus we may look into separation logic for this. Afterwards, I plan to show you what we try to do with Vercors, and for this, I may go through some examples of application and talk to you about my future work directions.

Hopefully, I will still have some time to discuss with you about how to approach the industry with our work, and maybe also in the in-between tell you about my former work just in case you ever happen to be interested in it as well.