Antoine Miné

Junior researcher at the CNRS.

Computer Science Department of the ENS.

Semantics and Abstract Interpretation team, headed by Patrick Cousot.

Common team with the ABSTRACTION project of the INRIA (Rocquencourt research center).

Research topic: automatic verification of the safety of software using formal methods.

Contents:

• Publications
• PhD. Thesis
• The Astrée static analyzer
• Research project(s)
  • THÉSÉE Project
• APRON library
• Teaching (in French)
• Emulating Hewlett Packard HP 48 calculators using the MESS system (including HP 48S/SX/G/GX/G+)
• Contact

Past Contents:

• Former research projects
  • APRON Project
  • ASTRÉE Project
  • DAEDALUS Project
• Octagon Abstract Domain Library version 0.9.10, now included within the APRON Library
• OCamlHTML Library
• Emulating 8-bit Thomson computers using the MESS system (including the MO5, MO6, TO7, TO7/70, TO8, TO9, TO9+, and some more)
• Undergraduate project
• Master's project (see also my PhD. Thesis).

Contact

PhD. Thesis: Weakly Relational Numerical Abstract Domains

[PDF (2.5 MB)] [PS.GZ (1.2 MB)] [BibTeX entry]

See also my defense page.

Publications

Full list: PDF file, PS.GZ file, BibTeX entries, BBL entries.

Pointer Analysis

[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, June 2006. ACM Press. [PS.GZ article (english)] [PDF article (english)] [PDF slides (english)] [BibTeX entry] [Editor link]

Verification of Embedded Systems

[2010] Why does Astrée scale up? In Formal Methods in System Design, volume 35, number 35, pages 229-264, Decembre 2010. Springer. Co-authored with P. Cousot, R. Cousot, J. Feret, L. Mauborgne, X. Rival. [.PDF article (english)] [BibTeX entry] [Editor link]

[2009] Space Software Validation using Abstract Interpretation. In Proc. of the Int. Space System Engineering Conf., Data Systems in Aerospace (DASIA 2009). Istambul, Turkey, May 2009, 7 pages. ESA. Co-authored with O. Bouissou, E. Conquet, P. Cousot, R. Cousot, J. Feret, K. Ghorbal, E. Goubault, D. Lesens, L. Mauborgne, S. Putot, X. Rival. [.PDF article (english)] [BibTeX entry] [Editor link]

[2007] Varieties of Static Analyzers: A Comparison with ASTRÉE. Invited article in Proc. of the 1st IEEE \& IFIP International Symposium on Theoretical Aspects of Software Engineering (TASE'07), Shanghai, China, June 2007, pages 3-17. IEEE Computer Society Press. Co-authored with P. Cousot, R. Cousot, J. Feret, L. Mauborgne, D. Monniaux, and X. Rival. [PS.GZ article (english)] [PDF article (english)] [BibTeX entry] [Editor link]

[2006] Combination of Abstractions in the ASTRÉE Static Analyzer. Invited article in post-proceedings of the 11th Annual Asian Computing Science Conference (ASIAN'06), Tokyo, Japan, December 2006, volume 4435 of Lecture Notes in Computer Science, pages 272-300. Co-authored with P. Cousot, R. Cousot, J. Feret, L. Mauborgne, D. Monniaux, and X. Rival. [PS.GZ article (english)] [PDF article (english)] [BibTeX entry] [Editor link]

[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, Scotland, April 2005. Springer. Co-authored with P. Cousot, R. Cousot, J. Feret, L. Mauborgne, D. Monniaux, and X. Rival. [PS.GZ article (english)] [PDF article (english)] [BibTeX entry] [Editor link]

[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, California, USA, June 2003. ACM Press. Co-authored with B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, D. Monniaux, and X. Rival. [PS.GZ article (english)] [PDF article (english)] [PDF slides (english)] [BibTeX entry] [Editor link]

[2002] Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software. Invited chapter 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, October 2002. Springer. Co-authored with B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, D. Monniaux, and X. Rival. [PS.GZ article (english)] [PDF article (english)] [BibTeX entry] [Editor link]

Numerical Abstract Domains

[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, Spain, January 2010. Springer. Co-authred with L. Chen, P. Cousot et J. Wang. [.PDF article (english)] [BibTeX entry] [Editor link]

[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, August 2009. Co-authored with L. Chen, P. Cousot, and J. Wang. [.PDF article (english)] [.PS.GZ article (english)] [PDF slides (english)] [BibTeX entry] [Editor link]

[2009] Apron: A Library of Numerical Abstract Domains for Static Analysis. Tool paper 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, June 2009. Co-authored with B. Jeannet. [.PDF article (english)] [BibTeX entry] [Editor link]

[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, December 2008. Co-authored with L. Chen and P. Cousot. [PS.GZ article (english)] [.PDF article (english)] [PDF slides (english)] [BibTeX entry] [Editor link]

[2006] The Octagon Abstract Domain. In Higher-Order and Symbolic Computation (HOSC), volume 19, number 1, pages 31-100, March 2006. Springer. [PS.GZ article (english)] [PDF article (english)] [BibTeX entry]

[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, South Caronila, USA, January 2006. Springer. [PS.GZ article (english)] [PDF article (english)] [BibTeX entry] [PDF slides (english)] [Editor link]

[2005] Weakly Relational Numerical Abstract Domains: Theory and Application. Invited talk 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, January 2005. [PS.GZ slides (english)] [PDF slides (english)]

[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, Barcelona, Spain, March 2004. Springer. [PS.GZ article (english)] [PDF article (english)] [PDF slides (english)] [BibTeX entry] [Editor link]

[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, Spain, September 2002. Springer. [PS.GZ article (english)] [PDF article (english)] [PS.GZ slides (english)] [PDF slides (english)] [BibTeX entry] [Editor link]

[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, Germany, October 2001. IEEE Press. See also the journal version. [PS.GZ article (english)] [PDF article (english)] [PS.GZ slides (english)] [BibTeX entry] [Editor link]

[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, May 2001. Springer. [PS.GZ article (english)] [PDF article (english)] [PS.GZ slides (english)] [BibTeX entry] [Editor link]

Reports

[2001] Representation of Two-Variable Difference or Sum Constraint Set and Application to Automatic Program Analysis, DEA report, 2001, [WEB page] [PS.GZ report (english)] [PDF report (english)] [PS.GZ slides (french)] [BibTeX entry]

[2001] Textures procédurales en temps réel avec OpenGL, Master report, 2001, [WEB page] [PS.GZ report (french)] [PDF report (french)]