Equation-Directed Axiomatization of Lustre Semantics to Enable Optimized Code Validation, a paper with L. Brun, C. Garion and X. Thirioux accepted at EMSOFT'23