Abstract machines and small-step semantics: a winning ticket for proof automation? - Alain Delaët; Sandrine Blazy; Denis Merigoux (PPDP, 2025)