Antoine Miné

Chargé de recherche 2^èmeclasse au CNRS.

Affecté au laboratoire d'informatique de l'ENS (UMR 8548) du Département d'informatique de l' ENS.

Équipe Sémantique et Interprétation Abstraite, dirigée par Patrick Cousot.

Équipe commune avec le projet ABSTRACTION de l'INRIA (site de Rocquencourt).

Thème de recherche: vérification de la sureté des logiciels par des méthodes formelles automatiques, analyse statique par interprétation abstraite.

Menu:

• Nouveau: The Second International Workshop on Numerical and Symbolic Abstract Domains (NSAD 2010) (page en anglais)
• Publications
• Thèse
• L'analyseur Astrée, commercialisé par AbsInt GmbH
• Bibliothèque APRON
• Enseignement
• Contact

Archives:

• Ancien projets de recherche
  • Projet THÉSÉE
  • Projet APRON
  • Projet ASTRÉE
  • Projet DAEDALUS
• Bibliothèque d'octogones version 0.9.10 (page en anglais), désormais incluse dans la bibliothèque APRON
• Bibliothèque OCamlHTML qui permet de programmer des scripts CGI en OCaml 3
• Émulation, avec le système MESS:
  • ordinateurs 8-bits Thomson (MO5, MO6, TO7, TO7/70, TO8, TO9, TO9+ et autres)
  • calculatrices Hewlett Packard HP 48 (HP 48S/SX/G/GX/G+) (page en anglais)
• Stage de maîtrise
• Stage de DEA (voir aussi ma thèse)

Contact

Thèse: Domaines numériques abstraits faiblement relationnels

[PDF (2.5 MB)] [PS.GZ (1.2 MB)] [entrée BibTeX]

Voir également la page de soutenance.

Publications

Liste complète: fichier PDF, fichier PS.GZ, entrées BibTeX, liste BBL.

Analyse de pointeurs

[2006] Field-Sensitive Value Analysis of Embedded C Programs with Union Types and Pointer Arithmetics. In Proc. of the ACM SIGPLAN/SIGBED Conf. on Languages, Compilers, and Tools for Embedded Systems (LCTES'06), pages 54-63, Ottawa, Ontario, Canada, juin 2006. ACM Press. [article PS.GZ (en anglais)] [article PDF (en anglais)] [transparents PDF (en anglais)] [entrée BibTeX] [lien éditeur]

Vérification de systèmes embarqués

[2010] Why does Astrée scale up? In Formal Methods in System Design, volume 35, numéro 35, pages 229-264, décembre 2010. Springer. Écrit en collaboration avec P. Cousot, R. Cousot, J. Feret, L. Mauborgne, X. Rival. [article PDF (en anglais)] [entrée BibTeX] [lien éditeur]

[2009] Space Software Validation using Abstract Interpretation. In Proc. of the Int. Space System Engineering Conf., Data Systems in Aerospace (DASIA 2009). Istambul, Turkey, mai 2009, 7 pages. ESA. Écrit en collaboration avec O. Bouissou, E. Conquet, P. Cousot, R. Cousot, J. Feret, K. Ghorbal, E. Goubault, D. Lesens, L. Mauborgne, S. Putot, X. Rival. [article PDF (en anglais)] [entrée BibTeX] [lien éditeur]

[2007] Varieties of Static Analyzers: A Comparison with ASTRÉE. Article invité in Proc. of the 1st IEEE \& IFIP International Symposium on Theoretical Aspects of Software Engineering (TASE'07), Shanghai, Chine, juin 2007, pages 3-17. IEEE Computer Society Press. Écrit en collaboration avec P. Cousot, R. Cousot, J. Feret, L. Mauborgne, D. Monniaux et X. Rival. [article PS.GZ (en anglais)] [article PDF (en anglais)] [entrée BibTeX] [lien éditeur]

[2006] Combination of Abstractions in the ASTRÉE Static Analyzer. Article invité in post-proceedings of the 11th Annual Asian Computing Science Conference (ASIAN'06), Tokyo, Japon, décembre 2006, volume 4435 of Lecture Notes in Computer Science, pages 272-300. Springer. Écrit en collaboration avec P. Cousot, R. Cousot, J. Feret, L. Mauborgne, D. Monniaux et X. Rival. [article PS.GZ (en anglais)] [article PDF (en anglais)] [entrée BibTeX] [lien éditeur]

[2005] The ASTRÉE Analyzer. In Proc. of the European Symposium on Programming (ESOP'05), volume 3444 of Lecture Notes in Computer Science, pages 21-30, Edinburgh, Écosse, avril 2005. Springer. Écrit en collaboration avec P. Cousot, R. Cousot, J. Feret, L. Mauborgne, D. Monniaux et X. Rival. [article PS.GZ (en anglais)] [article PDF (en anglais)] [entrée BibTeX] [lien éditeur]

[2003] A Static Analyzer for Large Safety-Critical Software. In Proc. of the ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI'03), pages 196-207, San Diego, Californie, USA, juin 2003. ACM Press. Écrit en collaboration avec B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, D. Monniaux et X. Rival. [article PS.GZ (en anglais)] [article PDF (en anglais)] [transparents PDF (en anglais)] [entrée BibTeX] [lien éditeur]

[2002] Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software. Chapitre invité in The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, pages 85-108, volume 2566 of Lecture Notes in Computer Science, octobre 2002. Springer. Écrit en collaboration avec B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, D. Monniaux et X. Rival. [article PS.GZ (en anglais)] [article PDF (en anglais)] [entrée BibTeX] [lien éditeur]

Domaines numériques abstraits

[2010] An Abstract Domain to Discover Interval Linear Equalities. In Proc. of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'10), volume 5944 of Lecture Notes in Computer Science, pages 112-128, Madrid, Espagne, janvier 2010. Springer. Écrit en collaboration avec L. Chen, P. Cousot et J. Wang. [article .PDF (en anglais)] [entrée BibTeX] [lien éditeur]

[2009] Interval Polyhedra: An Abstract Domain to Infer Interval Linear Relationships. In Proc. of the 16th International Static Analysis Symposium (SAS'09), volume 5673 of Lecture Notes in Computer Science, pages 309-325, Los Angeles, CA, USA, août 2009. Écrit en collaboration avec L. Chen, P. Cousot et J. Wang. [article PDF (en anglais)] [article PS.GZ (en anglais)] [transparents PDF (en anglais)] [entrée BibTeX] [lien éditeur]

[2009] Apron: A Library of Numerical Abstract Domains for Static Analysis. Article outil in Proc. of the 21st International Conference on Computer Aided Verification (CAV 2009), volume 5643 of Lecture Notes in Computer Science, pages 661-667, Grenoble, France, juin 2009. Écrit en collaboration avec B. Jeannet. [article PDF (en anglais)] [entrée BibTeX] [lien éditeur]

[2008] A Sound Floating-Point Polyhedra Abstract Domain. In Proc. of the Sixth Asian Symposium on Programming Languages and Systems (APLAS'08), volume 5356 of Lecture Notes in Computer Science, pages 3-18, Bangalore, India, décembre 2008. Écrit en collaboration avec L. Chen et P. Cousot. [article PS.GZ (en anglais)] [article PDF (en anglais)] [transparents PDF (en anglais)] [entrée BibTeX] [lien éditeur]

[2006] The Octagon Abstract Domain. In Higher-Order and Symbolic Computation (HOSC), volume 19, numéro 1, pages 31-100, mars 2006. Springer. [article PS.GZ (en anglais)] [article PDF (en anglais)] [entrée BibTeX]

[2006] Symbolic Methods to Enhance the Precision of Numerical Abstract Domains. In Proc. of the 7th Int. Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI'06), volume 3855 of Lecture Notes in Computer Science, pages 348-363, Charleston, Caroline du sud, USA, janvier 2006. Springer. [article PS.GZ (en englais)] [article PDF (en englais)] [entrée BibTeX] [expose PDF (en anglais)] [lien éditeur]

[2005] Weakly Relational Numerical Abstract Domains: Theory and Application. Éxposé invité in the 1st Workshop on Numerical and Symbolic Abstract Domains (NSAD'05), affiliated to the 6th Int. Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI'05), Paris, France, janvier 2005. [expose PS.GZ (en anglais)] [expose PDF (en anglais)]

[2004] Relational Abstract Domains for the Detection of Floating-Point Run-Time Errors. In Proc. of the European Symposium on Programming (ESOP'04), volume 2986 of Lecture Notes in Computer Science, pages 3-17, Barcelone, Espagne, mars 2004. Springer. [article PS.GZ (en englais)] [article PDF (en englais)] [transparents PDF (en englais)] [entrée BibTeX] [lien éditeur]

[2002] A Few Graph-Based Relational Numerical Abstract Domains. In Proc. of the 9th Int. Static Analysis Symposium (SAS'02), volume 2477 of Lecture Notes in Computer Science, pages 117-132, Madrid, Espagne, septembre 2002. Springer. [article PS.GZ (en englais)] [article PDF (en englais)] [transparents PS.GZ (en englais)] [transparents PDF (en englais)] [entrée BibTeX] [lien éditeur]

[2001] The Octagon Abstract Domain. In Proc. of the Workshop on Analysis, Slicing, and Transformation (AST'01), affiliated to the 8th Working Conference on Reverse Engineering (WCRE'01), pages 310-319, Stuttgart, Allemagne, octobre 2001. IEEE Press. Voir également la version journal. [article PS.GZ (en anglais)] [article PDF (en anglais)] [transparents PS.GZ (en anglais)] [entrée BibTeX] [lien éditeur]

[2001] A New Numerical Abstract Domain Based on Difference-Bound Matrices. In Proc. of the 2d Symp. on Programs as Data Objects (PADO II), volume 2053 of Lecture Notes in Computer Science, pages 155-172, Aarhus, Danemark, mai 2001. Springer. [article PS.GZ (en anglais)] [article PDF (en anglais)] [transparents PS.GZ (en anglais)] [entrée BibTeX] [lien éditeur]

Rapports

[2001] Representation of Two-Variable Difference or Sum Constraint Set and Application to Automatic Program Analysis rapport de DEA, 2001, [page WEB] [rapport PS.GZ (anglais)] [rapport PDF (anglais)] [transparents PS.GZ (français)] [entrée BibTeX]

[2001] Textures procédurales en temps réel avec OpenGL Master's report, 2001 [page WEB] [rapport PS.GZ (français)] [rapport PDF (français)]