Alexandre Moine, Arthur Charguéraud, François Pottier: Specification and verification of a transient stack. CPP 2022: 82-99