I am a Post-doc student at University of Oxford.
Until september 2015 I was at ULB, member of
ERC inVEST project, working in the MFV group,
in charge of the verification seminars.
My CV is available here: (English, French)
My work focuses on the sythesis of computerized systems.
In particular, I use game theoretical concepts to find good strategies in multi-agent systems.
During my thesis, I studied the concept of Nash equilibrium in concurrent games.
I also studied timed games.
This games are perfectly suited for the control of real time systems.
I developed algorithms for computing Nash equilibria in these kind of games with omega regular objectives and wrote a tool called PRALINE.
I am now mostly interested in:
- quantitative objectives in timed games and multiplayer-games;
- concepts for controller synthesis in distributed systems;
- developing tools for synthesis.
Pure Nash Equilibria in Concurrent Games. Logical Methods in Computer Science, 2015. To appear. ( PDF )
AbsSynthe: abstract synthesis from succinct safety specifications,
In 3rd Workshop in Synthesis.
PRALINE: A Tool for Computing Nash Equilibria in Concurrent Games. In CAV'13, LNCS 8044, pages 890-895. Springer, 2013. ( PDF | BibTeX + Abstract )
A Comparison of Succinctly Represented Finite-State Systems. In CONCUR'12, LNCS 7454, pages 147-161. Springer, 2012. ( PDF | PDF (long version) | BibTeX + Abstract )
Concurrent games with ordered objectives. In FoSSaCS'12, LNCS 7213, pages 301-315. Springer, 2012. ( PDF | PDF (long version) | BibTeX + Abstract )
Nash Equilibria in Concurrent Games with Büchi Objectives. In FSTTCS'11, Leibniz International Proceedings in Informatics 13, pages 375-386. Leibniz-Zentrum für Informatik, 2011. ( PDF | BibTeX + Abstract )
Computing Equilibria in Two-Player Timed Games
via Turn-Based Finite Games. In FORMATS'10, LNCS 6246, pages 62-76. Springer, 2010. ( PDF | PDF (long version) | BibTeX + Abstract )
Nash Equilibria for Reachability Objectives in Multi-player Timed
Games. In CONCUR'10, LNCS 6269, pages 192-206. Springer, 2010. ( PDF | PDF (long version) | BibTeX + Abstract )
Équilibres de Nash dans les Jeux Concurrents - Application aux
Jeux Temporisés. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan,
France, November 2012. ( PDF | BibTeX )
Calcul des équilibres de Nash dans les jeux temporisés. Rapport de Master, Master Parisien de Recherche en Informatique, Paris,
France, September 2009. ( PDF | PS | PS.GZ | BibTeX )
- April 2015, seminar in LIF, Marseille (France) Admissibility Concepts for Synthesis
- March 2015, MFV Seminar at ULB, Brussels (Belgium) Assume Admissible Synthesis
- March 2015, ERC meeting, Vienna (Austria) Assume Admissible Synthesis
- March 2015, seminar in LIAFA, Paris (France) Assume Admissible Synthesis
- January 2015, Dagstuhl seminar, Dagstuhl (Allemagne) The Complexity of Admissibility in Omega-Regular Games
- December 2014, seminar at INRIA, Grenoble (France) Controller synthesis: from circuits to quantitative, real-time and distributed systems
- July 2014, CSL-LICS, Vienna (Austria) The Complexity of Admissibility in Omega-Regular Games
- Avril 2014, HSCC, Berlin (Allemagne), Energy and Mean-Payoff Timed Games
MFV Seminar, ULB, March 21 2014
Energy and Mean Payoff Timed Games
The Complexity of Admissibility in omega-Regular Games GDR IM - GT-jeux: annual meeting, Paris, January 23 2014
- CFV Seminar, ULB
Repellor ALgorIthm for Nash Equilibria (download last version)
synthesis from succinct safety specifications
A tool to generate hardware description (AIGER and Verilog) from safety conditions given by regular languages.
A set of tools for generating AIGER circuits.
Tools for controller synthesis in multi-agent systems.
An Ocaml interface to BDD and ADD functions of the CUDD library.
An Ocaml library to read, write and manipulate AIGER files.
A patch for CUDD to use matrix multiplication in other rings than the default one.