I am a post-doctoral fellow in the SMV group (Software Modeling and Verification) at the CUI (Centre Universitaire d’Informatique) of the University of Geneva.
I am mainly interested formal verification, especially model-checking. My current focus is on automata enhanced with counters to verify quantitative properties of systems.
PhD Thesis
I defended my thesis on December 10th, 2013. thesis slides
Composition of the jury: A. Bouajjani, F. Vernadat, B. Bérard, M. Heiner, T. Junttila, F. Kordon, S. Baarir, Y. Thierry-Mieg
Software
Contributor to spaction, a prototype of model-checker that deals with properties with discrete quantitative information.
Contributor to StrataGEM, a decision diagrams based generic model-checker developed at CUI.
Contributor to its-tools, a decision diagrams based model-checking suite developed at LIP6.
Contributor to the platform CosyVerif.
Developer of Crocodile, a state-space generator for Symmetric Nets with Bags, as a proof of concept of the combination of symmetries and decision diagrams.