Managing the Etherlink core R&D projects (17 engineers).

R&D project manager.B-method training manager.Software development manager.Software verification manager.

2020-2021:ESIEE - Systèmes embarqués 3ème année - Vérifications formelles (20h)UPEC - Master 2ème année - Logiciels de preuve 2 (21h)2019-2020:ESIEE - Systèmes embarqués 3ème année - Vérifications formelles (20h)UPEC - Master 2ème année - Génie logiciel formel (21h)2018-2019:ESIEE - Systèmes embarqués 3ème année - Vérifications formelles (16h)UPEC - Master 2ème année - Génie logiciel formel (15h)2017-2018:ESIEE - Systèmes embarqués 3ème année - Vérifications formelles (16h)2011-2012:Université Paris Diderot - Master Ingénierie 1ère année - Compilation (20h)2010-2011:UPMC - Licence 1ère année - LI105 De la puce au web (42h)Université Paris Diderot - Master Ingénierie 1ère année - Compilation (20h)2008-2009:UPEC - Licence 3ème année - Algorithmique et complexité (36h)UPEC - Licence 2ème année - Architecture et systèmes d'exploitation (36h)UPEC - Licence 2ème année - Initiation à l'algorithmique (15h)UPEC - Licence 1ère année - Algorithmique expérimentale (13.5h)2007-2008:UPMC - Licence 1ère année - LI102 Programmation impérative (42h)2006-2007:UPMC - Licence 1ère année - LI101 Programmation récursive (21h)UPMC - Licence 1ère année - LI105 De la puce au web (21h)2005-2006:IFIPS - Cycle Ingé1 s6 - Projet système (16h)

Development of a reference database for the RER railway elements, with an emphasis on their functional specification.Model of the communication flows and agent processes at work in the RER control rooms.Internship supervision with ISTIA: a new, general purpose modelling language based on functional programming.Technical assistance at RATP.Key words: UML/Modelio, Arcadia/Capella, Python.

Development of safety critical railway systems using formal methods: informal and formal specifications, implementation, proof, test, documentation, traceability and validation of software components. Comparison between formalisms for proofs.Technical assistance at RATP, Alstom-Transport and Ansaldo STS.Consulting team management:- communication between the client and ClearSy;- anticipation of future needs in consultants and subcontractors;- integration of work produced by subcontractors.Key words: CBTC, zone controller, interlocking, model checking, B method.

CerCo [1] (certified complexity) project: development of the full C compiler prototype in OCaml.Internship supervision: the Cost plugin for the Frama-C [2] platform allows to call CerCo on a C program, synthesizes the cost of each function of the program, generates corresponding proof obligations and discharges some automatically.Key words: formally verified C compiler, temporal and spatial complexity, worst case execution time, source code annotation.[1] http://cerco.cs.unibo.it/[2] http://frama-c.com/

Development of methodologies and tools to ease the formal verification of critical embedded software. A mix of abstract interpretation, model checking, and observer automata is used to semi-automatically reduce the combinatorial state explosion by replacing a part of a system by a smaller one.Key words: formal verification, abstract interpretation, model checking, hardware description languages.

Development of methodologies and tools to ease the formal verification of critical embedded software. A mix of abstract interpretation, model checking, and observer automata is used to semi-automatically reduce the combinatorial state explosion by replacing a part of a system by a smaller one. Study of SystemC as a target language.Key words: formal verification, abstract interpretation, model checking, SystemC.

Development of tactics for the Coq proof assistant that allow to call external first-order logic provers (CVCLite, Simplify, Zenon). Translation of a goal of a higher-order logic, the Calculus of Inductive Constructions, into a less expressive formalism.Key words: higher- and first-order logics, Coq, decision procedures.