Specification and verification of a transient stack. - Alexandre Moine 001; Arthur Charguéraud; François Pottier (CPP, 2022)

A High-Level Separation Logic for Heap Space under Garbage Collection. - Alexandre Moine 001; Arthur Charguéraud; François Pottier (Proc. ACM Program. Lang., 2023)

Snapshottable Stores. - Clément Allain; Basile Clément; Alexandre Moine 001; Gabriel Scherer (Proc. ACM Program. Lang., 2024)

Formal verification of heap space bounds under garbage collection: a space tale from the stars. (Vérification formelle de bornes en espace de tas en présence d'un glaneur de cellules: un conte spatial venu des étoiles). - Alexandre Moine 001 (2024)

DisLog: A Separation Logic for Disentanglement. - Alexandre Moine 001; Sam Westrick; Stephanie Balzer (Proc. ACM Program. Lang., 2024)

Will It Fit? Verifying Heap Space Bounds of Concurrent Programs under Garbage Collection. - Alexandre Moine 001; Arthur Charguéraud; François Pottier (ACM Trans. Program. Lang. Syst., 2025)