Direction de recherche : Antoine MINÉ

Analyse statique de type et de valeur, par interprétation abstraite, de programmes Python avec des librairies C

Dans cette thèse, nous avons pour objectif de concevoir, à la fois théoriquement et expérimentalement, des méthodes pour la détection automatique de bogues potentiels dans les logiciels – ou la preuve de leur absence. Ces méthodes sont statiques : elles analysent le code source des programmes sans les exécuter. Nos travaux s’inscrivent dans le cadre de l’interprétation abstraite pour dériver une sémantique sûre et décidable. Le principal objet de ce travail est l’analyse des langages de programmation dynamiques. En particulier, ce travail se concentre sur les programmes écrits en Python, qui peuvent appeler des bibliothèques écrites en C.

Soutenance : 22/11/2021

Membres du jury :

MASTROENI Isabella (Università di Verona) [Rapporteur]
MØLLER Anders (Aarhus Universitet) [Rapporteur]
CHAILLOUX Emmanuel (Sorbonne Université)
MINÉ Antoine (Sorbonne Université)
LOGOZZO Francesco (Facebook Seattle)
MÜLLER Peter (ETH Zürich)
SCHMITT Alan (INRIA Rennes)

Publications 2017-2025

• 2025
  • M. Valnet, R. Monat, A. Miné : “Compositional Static Value Analysis for Higher-Order Numerical Programs”, Leibniz International Proceedings in Informatics, vol. 333, Bergen, Norway, pp. 15, (Dagstuhl Publishing) (2025)
  • R. Monat, A. Ouadjaout, A. Miné : “Mopsa-C with Trace Partitioning and Autosuggestions (Competition Contribution)”, Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2025, Hamilton, Ontario, Canada (2025)
  • R. Monat, A. Ouadjaout, A. Miné : “Easing Maintenance of Academic Static Analyzers”, International Journal on Software Tools for Technology Transfer, vol. CSV 2024 Special Issue, (Springer Verlag) (2025)
• 2024
  • R. Monat, M. Milanese, F. Parolini, J. Boillot, A. Ouadjaout, A. Miné : “Mopsa-C: Improved Verification for C Programs, Simple Validation of Correctness Witnesses (Competition Contribution)”, Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2024, vol. 14572, Lecture Notes in Computer Science, Luxembourg City, Luxembourg, pp. 387-392, (Springer Nature Switzerland) (2024)
• 2023
  • R. Monat, A. Ouadjaout, A. Miné : “Mopsa-C: Modular Domains and Relational Abstract Interpretation for C Programs (Competition Contribution)”, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023), vol. 13994, Lecture Notes in Computer Science, Paris, France, pp. 565-570, (Springer, Cham), (ISBN: 978-3-031-30820-8) (2023)
• 2021
  • R. Monat : “Static Type and Value Analysis by Abstract Interpretation of Python Programs with Native C Libraries”, soutenance de thèse, soutenance 22/11/2021, direction de recherche Miné, Antoine (2021)
  • R. Monat, A. Ouadjaout, A. Miné : “A Multilanguage Static Analysis of Python Programs with Native C Extensions”, Static Analysis Symposium (SAS), Chicago, Illinois, United States (2021)
  • D. Merigoux, R. Monat, J. Protzenko : “A Modern Compiler for the French Tax Code”, CC '21: 30^th ACM SIGPLAN International Conference on Compiler Construction, CC 2021: Proceedings of the 30^th ACM SIGPLAN International Conference on Compiler Construction, Virtual, Korea, Republic of, pp. 71-82, (ACM) (2021)
• 2020
  • R. Monat, A. Ouadjaout, A. Miné : “Static Type Analysis by Abstract Interpretation of Python Programs”, 34^th European Conference on Object-Oriented Programming (ECOOP 2020), vol. 166, Leibniz International Proceedings in Informatics (LIPIcs), Berlin (Virtual / Covid), Germany, (Schloss Dagstuhl--Leibniz-Zentrum für Informatik) (2020)
  • R. Monat, A. Ouadjaout, A. Miné : “Value and Allocation Sensitivity in Static Python Analyses”, Proceedings of the 9^th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis, London, United Kingdom, pp. 8-13, (ACM) (2020)
  • D. Merigoux, R. Monat, Ch. Gaie : “Étude formelle de l’implémentation du code des impôts”, JFLA 2020 - 31^e Journées Francophones des Langages Applicatifs, Gruissan, France (2020)
• 2019
  • M. Journault, A. Miné, R. Monat, A. Ouadjaout : “Combinations of Reusable Abstract Domains for a Multilingual Static Analyzer”, Verified Software. Theories, Tools, and Experiments, vol. 12031, Lecture Notes in Computer Science, New York, United States, pp. 1-18, (Springer) (2019)
• 2018
  • R. Monat : “Static Analysis by Abstract Interpretation Collecting Types of Python Programs”, (2018)
• 2017
  • R. Monat, A. Miné : “Precise Thread-Modular Abstract Interpretation of Concurrent Programs Using Relational Interference Abstractions”, Verification, Model Checking, and Abstract Interpretation, vol. 10145, Lecture Notes in Computer Science, Paris, France, pp. 386-404, (Springer) (2017)