Research activity

Méthodes de vérification automatique de la sûreté des logiciels informatiques : analyse statique sémantique des programmes, découverte d'invariants, interprétation abstraite, application à la vérification des logiciels embarqués critiques (logiciels avioniques, automobiles, ...).

5 PhD students (Supervision / Co-supervision)

• BAU Guillaume : Analyse statique par interprétation abstraite de smart-contrats Michelson
• MILANESE Marco : Under-Approximated Program Analysis and Counter-Example Generation by Abstract Interpretation
• PAROLINI Francesco : Static Analysis for Security Properties of Software by Abstract Interpretation
• RAZAFINTSIALONINA Mamy : Incremental Static Analysis for Program Verification
• VALNET Milla : Static Value Analysis by Abstract Interpretation of Functional Languages and Application to OCaml Analysis

7 PhD graduated 2012 - 2023

2015-2024 Publications

• 2024
  • M. Razafintsialonina, D. Bühler, A. Miné, V. Perrelle, J. Signoles : “Réutilisations de caches et d’invariants pour l’analyse statique incrémentale”, 35^es Journées Francophones des Langages Applicatifs (JFLA 2024), Saint-Jacut-de-la-Mer, France (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
  • M. Milanese, A. Miné : “Generation of Violation Witnesses by Under-Approximating Abstract Interpretation”, (2023)
  • F. Parolini, A. Miné : “Sound Abstract Nonexploitability Analysis”, (2023)
  • F. Parolini, A. Miné : “Sound Static Analysis of Regular Expressions for Vulnerabilities to Denial of Service Attacks (Extended Version)”, Science of Computer Programming, vol. 229, pp. 102960, (Elsevier) (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)
  • N. Shah, A. Misra, A. Miné, R. Venkat, R. Upadrasta : “BullsEye : Scalable and Accurate Approximation Framework for Cache Miss Calculation”, ACM Transactions on Architecture and Code Optimization, vol. 20 (1), pp. 1-28, (Association for Computing Machinery) (2023)
• 2022
  • G. Bau, A. Miné, V. Botbol, M. Bouaziz : “Abstract interpretation of Michelson smart-contracts”, SOAP '22: 11^th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis, San Diego, CA, United States, pp. 36-43, (ACM) (2022)
  • F. Parolini, A. Miné : “Sound Static Analysis of Regular Expressions for Vulnerabilities to Denial of Service Attacks”, (2022)
• 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. Delmas, A. Ouadjaout, A. Miné : “Static Analysis of Endian Portability by Abstract Interpretation”, 28^th Static Analysis Symposium (SAS 2021), vol. 12913, Lecture Notes in Computer Science, Chicago, Illinois, United States, pp. 102-123, (Springer International Publishing) (2021)
  • C. Urban, A. Miné : “A Review of Formal Methods applied to Machine Learning”, (2021)
• 2020
  • B. Kabi, E. Goubault, A. Miné, S. Putot : “Combining Zonotope Abstraction and Constraint Programming for Synthesizing Inductive Invariants”, Software Verification 12^th International Conference, VSTTE 2020, and 13^th International Workshop, NSV 2020, Los Angeles,, vol. 12549, Lecture Notes in Computer Science, Los Angeles, CA, United States, pp. 221-238, (Springer) (2020)
  • A. Ouadjaout, A. Miné : “A Library Modeling Language for the Static Analysis of C Programs”, 27^th Static Analysis Symposium, vol. 12389, Lecture Notes in Computer Science, Chicago, United States, pp. 223-247 (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)
• 2019
  • D. Delmas, A. Miné : “Analysis of Software Patches Using Numerical Abstract Interpretation”, International Static Analysis Symposium, vol. 11822, Lecture Notes in Computer Science, Porto, Portugal, pp. 225-246, (Springer) (2019)
  • A. Ouadjaout, A. Miné : “Quantitative Static Analysis of Communication Protocols using Abstract Markov Chains”, Formal Methods in System Design, vol. 54 (1), pp. 64-109, (Springer Verlag) (2019)
  • M. Journault, A. Miné, A. Ouadjaout : “An abstract domain for trees with numeric relations”, ESOP 2019 - 28^th European Symposium on Programming, vol. 11423, Lecture Notes in Computer Science, Prague, Czechia, pp. 724-751, (Springer) (2019)
  • D. Delmas, A. Miné : “Analysis of Program Differences with Numerical Abstract Interpretation”, PERR 2019 - 3^rd Workshop on Program Equivalence and Relational Reasoning, Prague, Czechia (2019)
  • Gh. Ziat, A. Maréchal, M. Pelleau, A. Miné, Ch. Truchet : “Combination of Boxes and Polyhedra Abstractions for Constraint Solving”, The 8^th International Workshop on Numerical and Symbolic Abstract Domains, Porto, Portugal (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
  • Th. Suzanne, A. Miné : “Relational Thread-Modular Abstract Interpretation Under Relaxed Memory Models”, Programming Languages and Systems, vol. 11275, Lecture Notes in Computer Science, Wellington, New Zealand, pp. 109-128 (2018)
  • M. Journault, A. Miné, A. Ouadjaout : “Modular static analysis of string manipulations in C programs”, SAS 2018, Freiburg im Breisgau, Germany (2018)
  • A. Miné, A. Ouadjaout, M. Journault : “Design of a Modular Platform for Static Analysis”, The Ninth Workshop on Tools for Automatic Program Analysis (TAPAS'18), Fribourg-en-Brisgau, Germany (2018)
  • Gh. Ziat, M. Pelleau, Ch. Truchet, A. Miné : “Finding solutions by finding inconsistencies”, CP 2018 - 24^th International Conference on Principles and Practice of Constraint Programming, Lille, France, pp. 1-16 (2018)
  • A. Fromherz, A. Ouadjaout, A. Miné : “Static Value Analysis of Python Programs by Abstract Interpretation”, NASA Formal Methods 10^th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings, vol. 10811, Lecture Notes in Computer Science, Newport News, VA, United States, pp. 185-202, (Springer) (2018)
• 2017
  • Gh. Ziat, M. Pelleau, Ch. Truchet, A. Miné : “Améliorer la propagation : l’Importance d’être Inconsistant”, Treizièmes journées Francophones de Programmation par Contraintes, Montreuil sur Mer, France (2017)
  • D. Kästner, A. Miné, A. SCHMIDT, H. Hille, L. Mauborgne, S. Wilhelm, X. Rival, J. Feret, P. Cousot, Ch. Ferdinand : “Finding All Potential Run-Time Errors and Data Races in Automotive Software”, SAE Technical Paper, Detroit, United States, pp. 1-9, (SAE International) (2017)
  • A. Miné : “Static Analysis of Embedded Real-Time Concurrent Software with Dynamic Priorities”, 6^th International Workshop on Numerical and Symbolic Abstract Domains (NSAD 2016), vol. 331, Electronic Notes in Theoretical Computer Science, Edimbourg, United Kingdom, pp. 3-39, (Elsevier) (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)
  • A. Ouadjaout, A. Miné : “Quantitative Static Analysis of Communication Protocols Using Abstract Markov Chains”, Static Analysis 24^th International Symposium, SAS 2017, New York, NY, USA, August 30 – September 1, 2017, Proceedings, vol. 10422, Lecture Notes in Computer Science, New York, NY, United States, pp. 277-298, (Springer) (2017)
  • A. Miné : “Tutorial on Static Inference of Numeric Invariants by Abstract Interpretation”, Foundations and Trends in Programming Languages, vol. 4 (3-4), pp. 120-372, (Now Publishers) (2017)
• 2016
  • X. Wu, L. Chen, A. Miné, W. Dong, J. Wang : “Static Analysis of Run-Time Errors in Interrupt-Driven Programs via Sequentialization”, ACM Transactions on Embedded Computing Systems (TECS), vol. 15 (4), ACM Transactions on Embedded Computing Systems (TECS) - Special Issue on ESWEEK2015 and Regular Papers, pp. 70:1-70:26, (ACM) (2016)
  • A. Miné, L. Mauborgne, X. Rival, J. Feret, P. Cousot, D. Kästner, S. Wilhelm, Ch. Ferdinand : “Taking Static Analysis to the Next Level: Proving the Absence of Run-Time Errors and Data Races with Astrée”, 8^th European Congress on Embedded Real Time Software and Systems (ERTS 2016), Toulouse, France (2016)
  • Th. Suzanne, A. Miné : “From Array Domains to Abstract Interpretation Under Store-Buffer-Based Memory Models”, Static Analysis, 23^rd International Symposium, SAS 2016, Edinburgh, UK, September 8-10, 2016, Proceedings, vol. 9837, Lecture Notes in Computer Science, Edinburgh, United Kingdom, pp. 469-488, (Springer) (2016)
  • M. Journault, A. Miné : “Static Analysis by Abstract Interpretation of the Functional Correctness of Matrix Manipulating Programs”, Static Analysis, 23^rd International Symposium, SAS 2016, Edinburgh, UK, September 8-10, 2016, Proceedings, vol. 9837, Lecture Notes in Computer Science, Edimbourg, United Kingdom, pp. 257-277, (Springer) (2016)
  • A. Miné, J. Breck, Th. Reps : “An Algorithm Inspired by Constraint Solvers to Infer Inductive Invariants in Numeric Programs”, Lecture Notes in Computer Science, vol. 9632, Programming Languages and Systems, Eindhoven, Netherlands, pp. 560-588, (Springer) (2016)
  • A. Ouadjaout, A. Miné, N. Lasla, N. Badache : “Static analysis by abstract interpretation of functional properties of device drivers in TinyOS”, Journal of Systems and Software, vol. 120, pp. 114-132, (Elsevier) (2016)
• 2015
  • X. Wu, L. Chen, A. Miné, W. Dong, J. Wang : “Numerical Static Analysis of Interrupt-Driven Programs via Sequentialization”, Embedded Software (EMSOFT), 2015 International Conference on, Amsterdam, Netherlands, pp. 55-64, (IEEE) (2015)
  • A. Miné, D. Delmas : “Towards an industrial use of sound static analysis for the verification of concurrent embedded avionics software”, Embedded Software (EMSOFT), 2015 International Conference on, Amsterdam, Netherlands, pp. 65-74, (IEEE) (2015)
  • C. Urban, A. Miné : “Inference of ranking functions for proving temporal properties by abstract interpretation”, Computer Languages, Systems and Structures, (Elsevier) (2015)
  • J. Bertrane, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, X. Rival : “Static Analysis and Verification of Aerospace Software by Abstract Interpretation”, Foundations and Trends in Programming Languages, vol. 2 (2-3), pp. 171-291, (Now Publishers) (2015)