Towards Formal Verification of a TPM Software Stack. - Yani Ziani; Nikolai Kosmatov; Frédéric Loulergue; Daniel Gracia Pérez; Téo Bernier (iFM, 2023)

Combining Deductive Verification with Shape Analysis. - Téo Bernier; Yani Ziani; Nikolai Kosmatov; Frédéric Loulergue (FASE, 2024)

Runtime Verification for High-Level Security Properties: Case Study on the TPM Software Stack. - Yani Ziani; Nikolai Kosmatov; Frédéric Loulergue; Daniel Gracia Pérez (TAP, 2024)