Typestates Specification and Verification in Frama-C. - Sébastien Patte; Virgile Prevosto (FormaliSE, 2025)