Being part of innovative R&D in formal methods for cloud reliability: managing R&D projects, solving technical challenges, collaborating with academia, and mentoring team members.
IAM policy analysis & SMT encoding optimization: Developed and applied inductive decision procedures to analyze cloud IAM policies for detecting and preventing privilege escalation. Implemented advanced SMT encoding optimizations using CVC5/Z3 Rust dedicated APIs to enhance solving performance and scalability.
Hybrid neuro-symbolic & agentic development: Contributed to integrating symbolic reasoning with agentic workflows to synthesize mathematically verifiable artifacts. Applied formal verification to provide a deterministic layer to autonomous processes, enhancing the precision of risk detection and safety within complex multi-agent environments.
Concurrency testing for large distributed applications: Applied lightweight formal methods, specifically Probabilistic Concurrency Testing (PCT), to verify ACID properties (Atomicity, Consistency, Isolation, and Durability) for large-scale P2P GSLB data plane. Leveraged formal abstraction techniques using the P framework.
Code-level verification: Used Gobra to verify code-level behavior in Go, leveraging network-layer abstractions and formal specifications, including separation logic, preconditions, postconditions, and invariants, to ensure correctness.
Technologies and tools: Formal abstraction, Probabilistic Concurrency Testing (PCT), SMT solving, Decision procedures, Inductive reasoning, Property directed reachability, IAM policies, GSLB, P2P protocols, P framework, Gobra, CVC5, Z3, Viper, TLA+, Rust, Go, Python ...
My activities are mainly in the topics:
Internet of Vehicles and urban trafic simulation
Machine learning applied to railway operation & smart urbain mobility
Formal design & verification of real-time, and safety-critical embedded systems : statistical model-checking, formal proofs ...
Component-based applications : synchronous & object-oriented "new" approaches applied to intelligent transportation systems, prototyping ...
Controller synthesis for cyber-physical systems : safety, reachability, learning, tooling ...
Interested in:
Category theory
Cybersecurity: theory, cryptography, exploitation, vulnerabilities, use of formal methods for protocol assessment ...
Wireless communication: theory, protocols, software-defined radio, 5/6G applied to vehicular communication (V2X)
AI & machine learning
PhD students:
Jean Tshibangu (2021/24)
Probabilistic predictive analysis of smart cities IoV networks
State doctoral funding (University of Paris-Saclay, UVSQ, LISV)
Sondoss Chtioui (2022/25)
Artificial intelligence for the analysis & management of railway control operational data
CIFRE industrial funding (University of Paris-Saclay, Egis Rail)
Philipp Ahrendt (2023/26)
Categorical modeling of autonomous distributed drone swarms
Co-funded by ESTACA and ISAE-SUPMECA
Partners:
EGIS Rail
LISV, UVSQ, University of Paris-Saclay
UTAC
5G/6G Innovation Center, University of Surrey ...
Member of the team Systèmes Intelligents Communicants conducted by Laboratoire de Recherche de l'ECE Paris.
Partners:
Laboratoire d'Ingénierie des Systèmes de Versailles (LISV) - UVSQ,
Département d'Informatique des Systèmes Complexes (DISC) - Institut FEMTO-ST,
CEA LIST, CEA Saclay,
Institut VEDECOM ...
PhD Students
Mohamed-Emine Laarouchi (2018-2020) A Safety Approach for CPS-IoT
Co-funded by CEA LIST, SAMOVAR, Telecom SudParis, Institut Polytechnique de Paris
Master and engineering student projects (2018-2020)
Formal design of vehicular communications
Prototyping delay-aware IEEE 802.11p V2X
Formal verification of the CBTC system of Line 13 of Paris subway:
Checking the compliance between the SCADE models of carborne and wayside sub-systems, and their software and system requirements.
Proof language: High Level Language HLL,
Proof assistant: Prover Certifier,
Proof startegies: k-induction, interpolation, and saturation of Stålmarck, ...
Optimization techniques: loop invariants, heuristics, ...
Position: Consultant at Atelier de Qualification Logicielle (AQL) - RATP.
Project: OURAGAN L13.
Partners: THALES Group and Prover Technology.
Design of an SMT-based model-checker for HLL.
Position: Intern at SafeRiver.
Partners: AQL - RATP.
Assessment of the CBTC solution URBALIS Fluence U500:
Failure Mode and Effect Analysis (FMEA) of the software layer,
Formal specification of an internal component-based synchronous language, ...
Position: Intern at ALSTOM Transport.
Project: Modernization of "Métro de Lille Métropole".
FMEA of the solution Tempo CBTC for Singapore's metro lines.
Position: Intern at SafeRiver.
Project: Land Transport Authority (LTA).
Partner: GE Transportation.
Verification and control of cyber-physical and hybrid systems:
Synthesis of safety controllers for switched systems using discrete symbolic models,
Development of the toolbox CoSyMA.
Institution: INRIA Grenoble.
Advised by Antoine Girard and Gregor Goessler.
Project: ANR VEDECY.
Formal verification of object-oriented component-based systems integrity and reuse:
Interoperability (compatibility and substitutability) check of components specified by behavioral contracts, merging their communicating protocols with the semantics of their operations,
Application to Enterprise JavaBeans EJB component model,
Recently (in 2015): re-adaptation and application to railway CBTC signaling systems.
Institution: Institut FEMTO-ST, DISC.
Supervised by Samir Chouali and Hassan Mountassir.
Project: ANR TACOS.
Verification of distributed systems using the pseudo-algorithmic language PlusCAL:
Extension PlusCAL to be compliant with the semantics of distribution,
Modification of the translator to TLA+ (Tamporal Logic of Actions),
Specifying and checking of some basic distributed algorithms.
Institution: LORIA.
Supervised by Stephan Merz and Martin Quinson.