نشـطات البـحـث

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

3 مسجلون في الدكتوراه (رئاسـة البـحث / تأطـير مـشـترك)

• DELMAS David : Analyse statique par interprétation abstraite de la portabilité des programmes
• JOURNAULT Matthieu : Analyse statique modulaire précise par interprétation abstraite pour la preuve automatique de correction et l'inférence de contrats
• MONAT Raphaël : Static Analysis by Abstract Interpretation of Dynamic Programming Languages

1 دكـتور 2019

إصدارات 2015-2019

• 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, Czech Republic, 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, Czech Republic (2019)
• 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)
  • M. Journault, A. Miné, A. Ouadjaout : “Modular static analysis of string manipulations in C programs”, SAS 2018, Freiburg im Breisgau, Germany (2018)
  • Th. Suzanne, A. Miné : “Relational Thread-Modular Abstract Interpretation Under Relaxed Memory Models”, APLAS 2018 - 16^th Asian Symposium on Programming Languages and Systems, vol. 11275, Lecture Notes in Computer Science, Wellington, New Zealand, pp. 109-128 (2018)
  • A. Fromherz, A. Ouadjaout, A. Miné : “Static Value Analysis of Python Programs by Abstract Interpretation”, NFM 2018 - 10^th International Symposium NASA Formal Methods, vol. 10811, Lecture Notes in Computer Science, Newport News, VA, USA, pp. 185-202, (Springer) (2018)
• 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)
  • 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”, WCX™ 2017 - SAE World Congress Experience, Detroit , USA, pp. 1-9, (SAE International) (2017)
  • R. Monat, A. Miné : “Precise Thread-Modular Abstract Interpretation of Concurrent Programs Using Relational Interference Abstractions”, Verification, Model Checking, and Abstract Interpretation (VMCAI) 2017, 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”, 24^th International Symposium on Static Analysis (SAS 2017), vol. 10422, Lecture Notes in Computer Science, New York, NY, USA, pp. 277-298, (Springer) (2017)
• 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)
  • 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é, J. Breck, Th. Reps : “An Algorithm Inspired by Constraint Solvers to Infer Inductive Invariants in Numeric Programs”, 25^th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, vol. 9632, Programming Languages and Systems, Eindhoven, Netherlands, pp. 560-588, (Springer) (2016)
  • Th. Suzanne, A. Miné : “From Array Domains to Abstract Interpretation Under Store-Buffer-Based Memory Models”, SAS 2016 - 23^rd Static Analysis Symposium, 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”, 23^rd Static Analysis Symposium (SAS), vol. 9837, Lecture Notes in Computer Science, Edimbourg, United Kingdom, pp. 257-277, (Springer) (2016)
  • 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) (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)
• 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)
  • X. Wu, L. Chen, A. Miné, W. Dong, J. Wang : “Numerical Static Analysis of Interrupt-Driven Programs via Sequentialization”, EMSOFT 2015 - International Conference on Embedded Software, 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”, ACM SIGBED International Conference on Embedded Software (EMSOFT), Amsterdam, Netherlands, pp. 65-74, (IEEE) (2015)