MetAcsl: Specification and Verification of High-Level Properties. - Virgile Robles; Nikolai Kosmatov; Virgile Prevosto; Louis Rilling; Pascale Le Gall (TACAS (1), 2019)

Tame Your Annotations with MetAcsl: Specifying, Testing and Proving High-Level Properties. - Virgile Robles; Nikolai Kosmatov; Virgile Prevosto; Louis Rilling; Pascale Le Gall (TAP@FM, 2019)

Methodology for Specification and Verification of High-Level Requirements with MetAcsl. - Virgile Robles; Nikolai Kosmatov; Virgile Prevosto; Louis Rilling; Pascale Le Gall (FormaliSE@ICSE, 2021)

Specifying and verifying high-level requirements on large programs : application to security of C programs. (Spécifier et vérifier des exigences de haut niveau sur des programmes importants : application à la sécurité des programmes C). - Virgile Robles (2022)

High-Level Program Properties in Frama-C: Definition, Verification and Deduction. - Virgile Robles; Nikolai Kosmatov; Virgile Prevosto; Pascale Le Gall (ISoLA (3), 2024)