A formally verified compiler for Lustre. - Timothy Bourke; Lélio Brun; Pierre-Évariste Dagand; Xavier Leroy; Marc Pouzet; Lionel Rieg (PLDI, 2017)

Towards a verified Lustre compiler with modular reset. - Timothy Bourke; Lélio Brun; Marc Pouzet (SCOPES, 2018)

Mechanized semantics and verified compilation for a dataflow synchronous language with reset. - Timothy Bourke; Lélio Brun; Marc Pouzet (Proc. ACM Program. Lang., 2020)

Mechanized semantics and verified compilation for a dataflow synchronous language with reset. (Sémantique mécanisée et compilation vérifiée pour un langage synchrone à flots de données avec réinitialisation). - Lélio Brun (2020)

Automated Security Analysis for Real-World IoT Devices. - Lélio Brun; Ichiro Hasuo; Yasushi Ono; Taro Sekiyama (HASP@MICRO, 2023)

Equation-Directed Axiomatization of Lustre Semantics to Enable Optimized Code Validation. - Lélio Brun; Christophe Garion; Pierre-Loïc Garoche; Xavier Thirioux (ACM Trans. Embed. Comput. Syst., 2023)