Atividade de Pesquisa

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, ...).

4 Doutorandos (Direção de pesquisa / Co-supervisão£o)

• BAU Guillaume : Analyse statique par interprétation abstraite de smart-contrats Michelson
• DELMAS David : Analyse statique par interprétation abstraite de la portabilité des programmes
• MONAT Raphaël : Static Analysis by Abstract Interpretation of Dynamic Programming Languages
• PAROLINI Francesco : Static Analysis for Security Properties of Software by Abstract Interpretation

3 Doutores em PhD 2019

Publicações 2015-2021

• 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)
  • 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)
  • 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 (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)
  • 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)