Introduction of statistical information in a syntactic analyzer for document image recognition. - André Oliveira Maroneze; Bertrand Coüasnon; Aurélie Lemaitre (DRR, 2011)

Formal Verification of a C Value Analysis Based on Abstract Interpretation. - Sandrine Blazy; Vincent Laporte; André Maroneze; David Pichardie (SAS, 2013)

Formal Verification of Loop Bound Estimation for WCET Analysis. - Sandrine Blazy; André Maroneze; David Pichardie (VSTTE, 2013)

A Formally Verified WCET Estimation Tool. - André Maroneze; Sandrine Blazy; David Pichardie; Isabelle Puaut (WCET, 2014)

Certified Compilation and Worst-Case Execution Time Estimation. (Compilation formellement vérifiée et estimation du pire temps d'éxécution). - André Oliveira Maroneze (2014)

Verified Validation of Program Slicing. - Sandrine Blazy; André Maroneze; David Pichardie (CPP, 2015)

Advances in Usability of Formal Methods for Code Verification with Frama-C. - André Maroneze; Valentin Perrelle; Florent Kirchner (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2019)

The dogged pursuit of bug-free C programs: the Frama-C software analysis platform. - Patrick Baudin; François Bobot; David Bühler; Loïc Correnson; Florent Kirchner; Nikolai Kosmatov; André Maroneze; Valentin Perrelle; Virgile Prevosto; Julien Signoles; Nicky Williams (Commun. ACM, 2021)