Maximilien Colange

I am assistant professor at the LRDE of EPITA.

I am mainly interested formal verification, especially model-checking. My current focus is on synthesis on systems from their formal specification, verification of ω-regular properties and of timed 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


Contributor to Spot, a library for the manipulation of LTL/PSL formulae and ω-automata.
My main contributions concern controller synthesis from LTL specifications.

Lead developper of TiAMo, a prototype of model-checker for Timed Automata and Weighted Timed Automata.

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.