\newcommand{\etalchar}[1]{$^{#1}$}
\begin{thebibliography}{SMM{\etalchar{+}}23b}

\bibitem[BCC{\etalchar{+}}02]{mine-LNCS02}
B{.} Blanchet, P{.} Cousot, R{.} Cousot, J{.} Feret, L{.} Mauborgne, A{.}
  Min{\'e}, D{.} Monniaux, and X{.} Rival.
\newblock Design and implementation of a special-purpose static program
  analyzer for safety-critical real-time embedded software.
\newblock In {\em The Essence of Computation: Complexity, Analysis,
  Transformation{.} Essays Dedicated to Neil D{.}~Jones}, volume 2566 of {\em
  Lecture Notes in Computer Science (LNCS)}, pages 85--108. Springer, Oct{.}
  2002.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/BlanchetCousotEtAl-LNCS-v2566-p85-108-2002.pdf}.

\bibitem[BCC{\etalchar{+}}03]{mine-PLDI03}
B{.} Blanchet, P{.} Cousot, R{.} Cousot, J{.} Feret, L{.} Mauborgne, A{.}
  Min{\'e}, D{.} Monniaux, and X{.} Rival.
\newblock A static analyzer for large safety-critical software.
\newblock In {\em Proc{.}~of the ACM SIGPLAN Conference on Programming Language
  Design and Implementation (PLDI'03)}, pages 196--207. ACM, Jun{.} 2003.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/pldi045-blanchet.pdf}.

\bibitem[BCC{\etalchar{+}}09]{mine-DASIA09}
O{.} Bouissou, {\'E}{.} Conquet, P{.} Cousot, R{.} Cousot, J{.} Feret, K{.}
  Ghorbal, {\'E}{.} Goubault, D{.} Lesens, L{.} Mauborgne, A{.} Min{\'e}, S{.}
  Putot, X{.} Rival, and M{.} Turin.
\newblock Space software validation using abstract interpretation.
\newblock In {\em Proc{.}~of the International Space System Engineering
  Conference on Data Systems in Aerospace (DASIA 2009)}, volume SP-669, page~7.
  ESA, May 2009.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/article-bouissou-al-dasia09.pdf}.

\bibitem[BCC{\etalchar{+}}10a]{mine-AIAA10}
J{.} Bertrane, P{.} Cousot, R{.} Cousot, J{.} Feret, L{.} Mauborgne, A{.}
  Min{\'e}, and X{.} Rival.
\newblock Static analysis and verification of aerospace software by abstract
  interpretation.
\newblock In {\em Proc{.}~of AIAA Infotech{$@$}Aerospace (I{$@$}A 2010)},
  number AIAA-2010-3385, page~38. American Institute of Aeronautics and
  Astronautics (AIAA), Apr{.} 2010.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/bertrane-al-aiaa10.pdf}.

\bibitem[BCC{\etalchar{+}}10b]{mine-UMLFM10}
J{.} Bertrane, P{.} Cousot, R{.} Cousot, J{.} Feret, L{.} Mauborgne, A{.}
  Min{\'e}, and X{.} Rival.
\newblock Static analysis by abstract interpretation of embedded critical
  software.
\newblock {\em the 3rd IEEE International Workshop on UML and Formal Methods
  (UML{\&}FM'10)}, 36(1):1--8, Nov{.} 2010.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/bertrane-al-umlfm10.pdf}.

\bibitem[BCC{\etalchar{+}}11]{mine-Boul11}
J{.} Bertrane, P{.} Cousot, R{.} Cousot, J{.} Feret, L{.} Mauborgne, A{.}
  Min{\'e}, and X{.} Rival.
\newblock L'analyseur statique {A}str{\'e}e.
\newblock In {\em Utilisations industrielles des techniques formelles :
  interpr{\'e}tation abstraite}, pages 67--114. Hermes Science, 17 Jun{.} 2011.

\bibitem[BCC{\etalchar{+}}15]{mine-FnTPL15}
J{.} Bertrane, P{.} Cousot, R{.} Cousot, J{.} Feret, L{.} Mauborgne, A{.}
  Min{\'e}, and X{.} Rival.
\newblock Static analysis and verification of aerospace software by abstract
  interpretation.
\newblock {\em Foundations and Trends in Programming Languages (FnTPL)},
  2(2--3):71--190, 2015.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/article-bertrane-al-fntpl15.pdf}.

\bibitem[BMBB22]{mine-SOAP22}
G{.} Bau, A{.} Min{\'e}, V{.} Botbol, and M{.} Bouaziz.
\newblock Abstract interpretation of {M}ichelson smart-contracts.
\newblock In {\em Proc{.}~of the 11th ACM SIGPLAN International Workshop on the
  State Of the Art in Program Analysis (SOAP'22)}, pages 36--43. ACM, Jun{.}
  2022.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-bau-al-soap2022.pdf}.

\bibitem[CCF{\etalchar{+}}05]{mine-ESOP05}
P{.} Cousot, R{.} Cousot, J{.} Feret, L{.} Mauborgne, A{.} Min{\'e}, D{.}
  Monniaux, and X{.} Rival.
\newblock The {A}str{\'e}e analyzer.
\newblock In {\em Proc{.}~of the European Symposium on Programming (ESOP'05)},
  volume 3444 of {\em Lecture Notes in Computer Science (LNCS)}, pages 21--30.
  Springer, Apr{.} 2005.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/esop05_astree.pdf}.

\bibitem[CCF{\etalchar{+}}06]{mine-ASIAN06}
P{.} Cousot, R{.} Cousot, J{.} Feret, L{.} Mauborgne, A{.} Min{\'e}, D{.}
  Monniaux, and X{.} Rival.
\newblock Combination of abstractions in the {A}str{\'e}e static analyzer.
\newblock In {\em Proc{.}~of the 11th Annual Asian Computing Science Conference
  (ASIAN'06)}, volume 4435 of {\em Lecture Notes in Computer Science (LNCS)},
  pages 272--300. Springer, Dec{.} 2006.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/CousotEtAl-asian06.pdf}.

\bibitem[CCF{\etalchar{+}}07]{mine-TASE07}
P{.} Cousot, R{.} Cousot, J{.} Feret, L{.} Mauborgne, A{.} Min{\'e}, D{.}
  Monniaux, and X{.} Rival.
\newblock Varieties of static analyzers: {A} comparison with {A}str{\'e}e.
\newblock In {\em Proc{.}~of the First IEEE {\&} IFIP International Symposium
  on Theoretical Aspects of Software Engineering (TASE'07)}, pages 3--20. IEEE
  CS Press, Jun{.} 2007.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/CousotP-Astree-TASE07.pdf}.

\bibitem[CCF{\etalchar{+}}09]{mine-FMSD09}
P{.} Cousot, R{.} Cousot, J{.} Feret, L{.} Mauborgne, A{.} Min{\'e}, and X{.}
  Rival.
\newblock Why does {A}str{\'e}e scale up?
\newblock {\em Formal Methods in System Design (FMSD)}, 35(3):229--264, Dec{.}
  2009.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/article-cousot-al-FMSD10.pdf}.

\bibitem[CLM{\etalchar{+}}14]{mine-SAS14b}
L{.} Chen, J{.} Liu, A{.} Min{\'e}, D{.} Kapur, and J{.} Wang.
\newblock An abstract domain to infer octagonal constraints with absolute
  value.
\newblock In {\em Proc{.}~of the 21st International Static Analysis Symposium
  (SAS'14)}, volume 8373 of {\em Lecture Notes in Computer Science (LNCS)},
  pages 101--117. Springer, Sep{.} 2014.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-chen-al-sas14.pdf}.

\bibitem[CMC08]{mine-APLAS08}
L{.} Chen, A{.} Min{\'e}, and P{.} Cousot.
\newblock A sound floating-point polyhedra abstract domain.
\newblock In {\em Proc{.}~of the Sixth Asian Symposium on Programming Languages
  and Systems (APLAS'08)}, volume 5356 of {\em Lecture Notes in Computer
  Science (LNCS)}, pages 3--18. Springer, Dec{.} 2008.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-chen-al-aplas08.pdf}.

\bibitem[CMWC09]{mine-SAS09}
L{.} Chen, A{.} Min{\'e}, J{.} Wang, and P{.} Cousot.
\newblock Interval polyhedra: {A}n abstract domain to infer interval linear
  relationships.
\newblock In {\em Proc{.}~of the 16th International Static Analysis Symposium
  (SAS'09)}, volume 5673 of {\em Lecture Notes in Computer Science (LNCS)},
  pages 309--325. Springer, Aug{.} 2009.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-chen-al-sas09.pdf}.

\bibitem[CMWC10]{mine-VMCAI10}
L{.} Chen, A{.} Min{\'e}, J{.} Wang, and P{.} Cousot.
\newblock An abstract domain to discover interval linear equalities.
\newblock In {\em Proc{.}~of the 11th International Conference on Verification,
  Model Checking, and Abstract Interpretation (VMCAI'10)}, volume 5944 of {\em
  Lecture Notes in Computer Science (LNCS)}, pages 112--128. Springer, Jan{.}
  2010.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-chen-al-vmcai10.pdf}.

\bibitem[CMWC11]{mine-ESOP11b}
L{.} Chen, A{.} Min{\'e}, J{.} Wang, and P{.} Cousot.
\newblock Linear absolute value relation analysis.
\newblock In {\em Proc{.}~of the 20th European Symposium on Programming
  (ESOP'11)}, volume 6602 of {\em Lecture Notes in Computer Science (LNCS)},
  pages 156--175. Springer, Mar{.} 2011.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/chen-al-esop11.pdf}.

\bibitem[Del22]{mine-PhDDelmas}
D{.} Delmas.
\newblock {\em Static analysis of program portability by abstract
  interpretation}.
\newblock PhD thesis, Sorbonne Universit{\'e}, Dec{.} 2022.
\newblock \url{https://www.di.ens.fr/~delmas/phd/thesis-delmas.pdf}.

\bibitem[DM19a]{mine-PERR19}
D{.} Delmas and A{.} Min{\'e}.
\newblock Analysis of program differences with numerical abstract
  interpretation.
\newblock In {\em Proc{.}~of 3rd Workshop on Program Equivalence and Relational
  Reasoning (PERR19)}, pages 1--5, Apr{.} 2019.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/article-delmas-mine-PERR19.pdf}.

\bibitem[DM19b]{mine-SAS19}
D{.} Delmas and A{.} Min{\'e}.
\newblock Analysis of software patches using numerical abstract interpretation.
\newblock In {\em Proc{.}~of the 26th International Static Analysis Symposium
  (SAS'19)}, volume 11822 of {\em Lecture Notes in Computer Science (LNCS)},
  pages 225--246. Springer, Oct{.} 2019.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/article-delmas-mine-sas19.pdf}.

\bibitem[DOM21]{mine-SAS21b}
D{.} Delmas, A{.} Ouadjaout, and A{.} Min{\'e}.
\newblock Static analysis of endian portability by abstract interpretation.
\newblock In {\em Proc{.}~of the 28th International Static Analysis Symposium
  (SAS'21)}, volume 12913 of {\em Lecture Notes in Computer Science (LNCS)},
  pages 102--123. Springer, Oct{.} 2021.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-delmas-al-sas21.pdf}.

\bibitem[FOM18]{mine-NFM18}
A{.} Fromherz, A{.} Ouadjaout, and A{.} Min{\'e}.
\newblock Static value analysis of {P}ython programs by abstract
  interpretation.
\newblock In {\em Proc{.}~of 10th NASA Formal Methods Symposium (NFM'18)},
  Lecture Notes in Computer Science (LNCS), pages 185--202. Springer, Apr{.}
  2018.
\newblock \url{https://hal.sorbonne-universite.fr/hal-01782390}.

\bibitem[JM09]{mine-CAV09}
B{.} Jeannet and A{.} Min{\'e}.
\newblock Apron: {A} library of numerical abstract domains for static analysis.
\newblock In {\em Proc{.}~of the 21st International Conference on Computer
  Aided Verification (CAV 2009)}, volume 5643 of {\em Lecture Notes in Computer
  Science (LNCS)}, pages 661--667. Springer, Jun{.} 2009.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/article-mine-jeannet-cav09.pdf}.

\bibitem[JM16]{mine-SAS16b}
M{.} Journault and A{.} Min{\'e}.
\newblock Static analysis by abstract interpretation of the functional
  correctness of matrix manipulating programs.
\newblock In {\em Proc{.}~of the 23st International Static Analysis Symposium
  (SAS'16)}, volume 9837 of {\em Lecture Notes in Computer Science (LNCS)},
  pages 257--277. Springer, Sep{.} 2016.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/article-journault-al-sas16.pdf}.

\bibitem[JM18]{mine-FMSD18}
M{.} Journault and A{.} Min{\'e}.
\newblock Inferring functional properties of matrix manipulating programs by
  abstract interpretation.
\newblock {\em Formal Methods in System Design (FMSD)}, 53(2):221--258, Oct{.}
  2018.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/article-journault-al-fmsd18.pdf}.

\bibitem[JMMO19]{mine-VSTTE19}
M{.} Journault, A{.} Min{\'e}, R{.} Monat, and A{.} Ouadjaout.
\newblock Combinations of reusable abstract domains for a multilingual static
  analyzer.
\newblock In {\em Proc{.}~of the 11th Working Conference on Verified Software:
  Theories, Tools, and Experiments (VSTTE19)}, volume 12031 of {\em Lecture
  Notes in Computer Science (LNCS)}, pages 1--18. Springer, Jul{.} 2019.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-mine-al-vstte19.pdf}.

\bibitem[JMO18]{mine-SAS18}
M{.} Journault, A{.} Min{\'e}, and A{.} Ouadjaout.
\newblock Modular static analysis of string manipulations in {C} programs.
\newblock In {\em Proc{.}~of the 25th International Static Analysis Symposium
  (SAS'18)}, volume 11002 of {\em Lecture Notes in Computer Science (LNCS)},
  pages 243--262. Springer, Sep{.} 2018.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/article-journault-al-sas18.pdf}.

\bibitem[JMO19]{mine-ESOP19}
M{.} Journault, A{.} Min{\'e}, and A{.} Ouadjaout.
\newblock An abstract domain for trees with numeric relations.
\newblock In {\em Proc{.}~of the 28rd European Symposium on Programming
  (ESOP'19)}, volume 11423 of {\em Lecture Notes in Computer Science (LNCS)},
  pages 724--751. Springer, Apr{.} 2019.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/article-journault-al-esop19.pdf}.

\bibitem[Jou19]{mine-PhDJournault}
M{.} Journault.
\newblock {\em Precise and modular static analysis by abstract interpretation
  for the automatic proof of program soundness and contracts inference}.
\newblock PhD thesis, Sorbonne Universit{\'e}, Nov{.} 2019.
\newblock \url{https://www-apr.lip6.fr/~journault/publi/manuscrit.pdf}.

\bibitem[KFW{\etalchar{+}}09]{mine-ESS09}
D{.} K{\"a}stner, C{.} Ferdinand, S{.} Wilhelm, S{.} Nenova, O{.} Honcharova,
  P{.} Cousot, R{.} Cousot, J{.} Feret, L{.} Mauborgne, A{.} Min{\'e}, X{.}
  Rival, and {\'E}{.}-J{.} Sims.
\newblock Astr{\'e}e: {N}achweis der abwesenheit von laufzeitfehlern.
\newblock In {\em Proc{.}~of Workshop Entwicklung zuverl{\"a}ssiger
  Software-Systeme (ESS'09)}, page~6, Jun{.} 2009.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/KaestnerEtAl2009.pdf}.

\bibitem[KGMP20]{mine-NSV20}
B{.} Kabi, {\'E}{.} Goubault, A{.} Min{\'e}, and S{.} Putot.
\newblock Combining zonotope abstraction and constraint programming for
  synthesizing inductive invariants.
\newblock In {\em Proc{.}~of the 13th International Workshop on Numerical
  Software Verification (NSV'20)}, volume 12549 of {\em Lecture Notes in
  Computer Science (LNCS)}, pages 221--238. Springer, Jul{.} 2020.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/bibek-al-nsv-2020.pdf}.

\bibitem[KMS{\etalchar{+}}17]{mine-SAE17}
D{.} K{\"a}stner, A{.} Min{\'e}, A{.} Schmidt, H{.} Hille, L{.} Mauborgne, S{.}
  Wilhelm, X{.} Rival, J{.} Feret, P{.} Cousot, and C{.} Ferdinand.
\newblock Finding all potential run-time errors and data races in automotive
  software.
\newblock In {\em Proc{.}~of Automotive Software, SAE world Congress (SAE'17)},
  SAE Technical Paper, page~9. SAE International, Apr{.} 2017.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/article-kastner-al-sae17.pdf}.

\bibitem[KWN{\etalchar{+}}10]{mine-ERTS10}
D{.} K{\"a}stner, S{.} Wilhelm, S{.} Nenova, P{.} Cousot, R{.} Cousot, J{.}
  Feret, L{.} Mauborgne, A{.} Min{\'e}, and X{.} Rival.
\newblock Astr{\'e}e: {P}roving the absence of runtime errors.
\newblock In {\em Proc{.}~of Embedded Real Time Software and Systems (ERTS2
  2010)}, page~9, May 2010.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/kastner-al-erts10.pdf}.

\bibitem[LCMW20]{mine-NN20}
J{.} Liu, L{.} Chen, A{.} Min{\'e}, and J{.} Wang.
\newblock Input validation for neural networks via runtime local robustness
  verification.
\newblock Technical report, Computing Research Repository (arXiv) (CoRR),
  Apr{.} 2020.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-liu-et-al-2020.pdf}.

\bibitem[MBR16]{mine-ESOP16}
A{.} Min{\'e}, J{.} Breck, and T{.} Reps.
\newblock An algorithm inspired by constraint solvers to infer inductive
  invariants in numeric programs.
\newblock In {\em Proc{.}~of the 25rd European Symposium on Programming
  (ESOP'16)}, volume 9632 of {\em Lecture Notes in Computer Science (LNCS)},
  pages 560--588. Springer, Apr{.} 2016.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-mine-al-esop16.pdf}.

\bibitem[MD15]{mine-EMSOFT15a}
A{.} Min{\'e} and D{.} Delmas.
\newblock Towards an industrial use of sound static analysis for the
  verification of concurrent embedded avionics software.
\newblock In {\em Proc{.}~of the 15th International Conference on Embedded
  Software (EMSOFT'15)}, pages 65--74. IEEE CS Press, Oct{.} 2015.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/article-mine-delmas-emsoft15.pdf}.

\bibitem[Min98]{mine-Licence98}
A{.} Min{\'e}.
\newblock Textures proc{\'e}durales en temps r{\'e}el avec {O}pen{G}{L}, Sep{.}
  1998.
\newblock \url{http://www-apr.lip6.fr/~mine/stage_imagis/rapport_maitrise.pdf}.

\bibitem[Min00]{mine-Master00}
A{.} Min{\'e}.
\newblock Representation of two-variable difference or sum constraint set and
  application to automatic program analysis, Sep{.} 2000.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/report-mine-dea.pdf}.

\bibitem[Min01a]{mine-PADO01}
A{.} Min{\'e}.
\newblock A new numerical abstract domain based on difference-bound matrices.
\newblock In {\em Proc{.}~of the Second Symposium on Programs as Data Objects
  (PADO II)}, volume 2053 of {\em Lecture Notes in Computer Science (LNCS)},
  pages 155--172. Springer, May 2001.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-mine-padoII.pdf}.

\bibitem[Min01b]{mine-AST01}
A{.} Min{\'e}.
\newblock The octagon abstract domain.
\newblock In {\em Proc{.}~of the Workshop on Analysis, Slicing, and
  Transformation (AST'01)}, pages 310--319. IEEE CS Press, Oct{.} 2001.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-mine-ast01.pdf}.

\bibitem[Min02]{mine-SAS02}
A{.} Min{\'e}.
\newblock A few graph-based relational numerical abstract domains.
\newblock In {\em Proc{.}~of the 9th International Static Analysis Symposium
  (SAS'02)}, volume 2477 of {\em Lecture Notes in Computer Science (LNCS)},
  pages 117--132. Springer, Sep{.} 2002.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-mine-sas02.pdf}.

\bibitem[Min04a]{mine-ESOP04}
A{.} Min{\'e}.
\newblock Relational abstract domains for the detection of floating-point
  run-time errors.
\newblock In {\em Proc{.}~of the European Symposium on Programming (ESOP'04)},
  volume 2986 of {\em Lecture Notes in Computer Science (LNCS)}, pages 3--17.
  Springer, Mar{.} 2004.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-mine-esop04.pdf}.

\bibitem[Min04b]{mine-PhD04}
A{.} Min{\'e}.
\newblock {\em Weakly relational numerical abstract domains}.
\newblock PhD thesis, {\'E}cole Polytechnique, Dec{.} 2004.
\newblock \url{http://www-apr.lip6.fr/~mine/these/these-color.pdf}.

\bibitem[Min06a]{mine-LCTES06}
A{.} Min{\'e}.
\newblock Field-sensitive value analysis of embedded {C} programs with union
  types and pointer arithmetics.
\newblock In {\em Proc{.}~of the ACM SIGPLAN/SIGBED Conference on Languages,
  Compilers, and Tools for Embedded Systems (LCTES'06)}, pages 54--63. ACM,
  Jun{.} 2006.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-mine-lctes06.pdf}.

\bibitem[Min06b]{mine-HOSC06}
A{.} Min{\'e}.
\newblock The octagon abstract domain.
\newblock {\em Higher-Order and Symbolic Computation (HOSC)}, 19(1):31--100,
  2006.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-mine-HOSC06.pdf}.

\bibitem[Min06c]{mine-VMCAI06}
A{.} Min{\'e}.
\newblock Symbolic methods to enhance the precision of numerical abstract
  domains.
\newblock In {\em Proc{.}~of the 7th International Conference on Verification,
  Model Checking, and Abstract Interpretation (VMCAI'06)}, volume 3855 of {\em
  Lecture Notes in Computer Science (LNCS)}, pages 348--363. Springer, Jan{.}
  2006.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-mine-VMCAI06.pdf}.

\bibitem[Min11]{mine-ESOP11a}
A{.} Min{\'e}.
\newblock Static analysis of run-time errors in embedded critical parallel {C}
  programs.
\newblock In {\em Proc{.}~of the 20th European Symposium on Programming
  (ESOP'11)}, volume 6602 of {\em Lecture Notes in Computer Science (LNCS)},
  pages 398--418. Springer, Mar{.} 2011.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-mine-esop11.pdf}.

\bibitem[Min12a]{mine-WING12}
A{.} Min{\'e}.
\newblock Abstract domains for bit-level machine integer and floating-point
  operations.
\newblock In {\em Proc{.}~of the 4th International Workshop on Invariant
  Generation (WING'12)}, number HW-MACS-TR-0097, page~16. EasyChair Proceedings
  in Computing, 30 Jun{.} 2012.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-mine-wing12.pdf}.

\bibitem[Min12b]{mine-NSAD12}
A{.} Min{\'e}.
\newblock Inferring sufficient conditions with backward polyhedral
  under-approximations.
\newblock In {\em Proc{.}~of the 4th International Workshop on Numerical and
  Symbolic Abstract Domains (NSAD'12)}, volume 287 of {\em Electronic Notes in
  Theoretical Computer Science (ENTCS)}, pages 89--100. Elsevier, 10 Sept{.}
  2012.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-mine-nsad12.pdf}.

\bibitem[Min12c]{mine-MOVEP12}
A{.} Min{\'e}.
\newblock Static analysis by abstract interpretation of sequential and
  multi-thread programs.
\newblock In {\em Proc{.}~of the 10th School of Modelling and Verifying
  Parallel Processes (MOVEP 2012)}, pages 35--48, 3--7 Dec{.} 2012.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-mine-MOVEP12.pdf}.

\bibitem[Min12d]{mine-LMCS12}
A{.} Min{\'e}.
\newblock Static analysis of run-time errors in embedded real-time parallel {C}
  programs.
\newblock {\em Logical Methods in Computer Science (LMCS)}, 8(26):63, Mar{.}
  2012.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-mine-LMCS12.pdf}.

\bibitem[Min13a]{mine-SCP13}
A{.} Min{\'e}.
\newblock Backward under-approximations in numeric abstract domains to
  automatically infer sufficient program conditions.
\newblock {\em Science of Computer Programming (SCP)}, page~33, Oct{.} 2013.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-mine-SCP13.pdf}.

\bibitem[Min13b]{mine-HdR13}
A{.} Min{\'e}.
\newblock Static analysis by abstract interpretation of concurrent programs.
\newblock Technical report, {\'E}cole normale sup{\'e}rieure, May 2013.
\newblock \url{http://www-apr.lip6.fr/~mine/hdr/hdr-compact-col.pdf}.

\bibitem[Min14]{mine-VMCAI14}
A{.} Min{\'e}.
\newblock Relational thread-modular static value analysis by abstract
  interpretation.
\newblock In {\em Proc{.}~of the 15th International Conference on Verification,
  Model Checking, and Abstract Interpretation (VMCAI'14)}, volume 8318 of {\em
  Lecture Notes in Computer Science (LNCS)}, pages 39--58. Springer, Jan{.}
  2014.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-mine-VMCAI14.pdf}.

\bibitem[Min15]{mine-VMCAI15b}
A{.} Min{\'e}.
\newblock Astr{\'e}e{A}: {A} static analyzer for large embedded multi-task
  software.
\newblock In {\em Proc{.}~of the 16th International Conference on Verification,
  Model Checking, and Abstract Interpretation (VMCAI'15)}, volume 8931 of {\em
  Lecture Notes in Computer Science (LNCS)}, page~3. Springer, Jan{.} 2015.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-mine-vmcai15.pdf}.

\bibitem[Min16]{mine-NSAD16}
A{.} Min{\'e}.
\newblock Static analysis of embedded real-time concurrent software with
  dynamic priorities.
\newblock In {\em Proc{.}~of the 6th International Workshop on Numerical and
  Symbolic Abstract Domains (NSAD'16)}, Electronic Notes in Theoretical
  Computer Science (ENTCS), pages 3--39. Elsevier, 11 Sept{.} 2016.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-mine-nsad16.pdf}.

\bibitem[Min17]{mine-FnTPL17}
A{.} Min{\'e}.
\newblock Tutorial on static inference of numeric invariants by abstract
  interpretation.
\newblock {\em Foundations and Trends in Programming Languages (FnTPL)},
  4(3--4):120--372, 2017.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-mine-FTiPL17.pdf}.

\bibitem[MM17]{mine-VMCAI17}
R{.} Monat and A{.} Min{\'e}.
\newblock Precise thread-modular abstract interpretation of concurrent programs
  using relational interference abstractions.
\newblock In {\em Proc{.}~of the 18th International Conference on Verification,
  Model Checking, and Abstract Interpretation (VMCAI'17)}, volume 10145 of {\em
  Lecture Notes in Computer Science (LNCS)}, pages 386--404. Springer, Jan{.}
  2017.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/article-monat-mine-vmcai17.pdf}.

\bibitem[MM24]{mine-VMCAI24b}
M{.} Milanese and A{.} Min{\'e}.
\newblock Generation of violation witnesses by under-approximating abstract
  interpretation.
\newblock In {\em Proc{.}~of the 25th International Conference on Verification,
  Model Checking, and Abstract Interpretation (VMCAI'24)}, volume 14499 of {\em
  Lecture Notes in Computer Science (LNCS)}. Springer, Jan{.} 2024.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/article-milanese-al-vmcai24.pdf}.

\bibitem[MMR{\etalchar{+}}16]{mine-ERTS16}
A{.} Min{\'e}, L{.} Mauborgne, X{.} Rival, J{.} Feret, P{.} Cousot, D{.}
  K{\"a}stner, S{.} Wilhelm, and C{.} Ferdinand.
\newblock Taking static analysis to the next level: {P}roving the absence of
  run-time errors and data races with {A}str{\'e}e.
\newblock In {\em Proc{.}~of Embedded Real Time Software and Systems (ERTS2
  2016)}, pages 570--579, Jan 2016.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-mine-al-erts16.pdf}.

\bibitem[MN99]{mine-INRIA99}
A{.} Min{\'e} and F{.} Neyret.
\newblock Perlin textures in real time using {O}pen{G}{L}.
\newblock Technical Report 2713, INRIA, Jun{.} 1999.
\newblock \url{http://hal.inria.fr/inria-00072955}.

\bibitem[MOJ18]{mine-TAPAS18}
A{.} Min{\'e}, A{.} Ouadjaout, and M{.} Journault.
\newblock Design of a modular platform for static analysis.
\newblock In {\em Proc{.}~of 9h Workshop on Tools for Automatic Program
  Analysis (TAPAS'18)}, Lecture Notes in Computer Science (LNCS), page~4, 28
  Aug{.} 2018.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/mine-al-tapas18.pdf}.

\bibitem[MOM20a]{mine-ECOOP20}
R{.} Monat, A{.} Ouadjaout, and A{.} Min{\'e}.
\newblock Static type analysis by abstract interpretation of {P}ython programs.
\newblock In {\em Proc{.}~of the 34th European Conference on Object-Oriented
  Programming (ECOOP'20)}, volume 166 of {\em Leibniz International Proceedings
  in Informatics (LIPIcs)}, pages 17:1--17:29. Dagstuhl Publishing, Jul{.}
  2020.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/article-monat-al-ecoop20.pdf}.

\bibitem[MOM20b]{mine-SOAP20}
R{.} Monat, A{.} Ouadjaout, and A{.} Min{\'e}.
\newblock Value and allocation sensitivity in static {P}ython analyses.
\newblock In {\em Proc{.}~of the 9th ACM SIGPLAN International Workshop on the
  State Of the Art in Program Analysis (SOAP'20)}, pages 8--13. ACM, Jun{.}
  2020.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-monat-al-soap20.pdf}.

\bibitem[MOM21]{mine-SAS21a}
R{.} Monat, A{.} Ouadjaout, and A{.} Min{\'e}.
\newblock A multilanguage static analysis of {P}ython programs with native {C}
  extensions.
\newblock In {\em Proc{.}~of the 28th International Static Analysis Symposium
  (SAS'21)}, volume 12913 of {\em Lecture Notes in Computer Science (LNCS)},
  pages 323--345. Springer, Oct{.} 2021.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-monat-al-sas21.pdf}.

\bibitem[Mon18]{mine-MasterMonat}
R{.} Monat.
\newblock Static analysis by abstract interpretation collecting types of
  {P}ython programs, Sep{.} 2018.
\newblock \url{https://hal.archives-ouvertes.fr/hal-01869049}.

\bibitem[Mon21]{mine-PhDMonat}
R{.} Monat.
\newblock {\em Static type and value analysis by abstract interpretation of
  {P}ython programs with native {C} libraries}.
\newblock PhD thesis, Sorbonne Universit{\'e}, Nov{.} 2021.
\newblock \url{https://rmonat.fr/data/pubs/2021/thesis_monat.pdf}.

\bibitem[MRC10]{mine-NSAD10}
A{.} Min{\'e} and E{.} Rodr{\'i}guez~Carbonell, editors.
\newblock {\em Proc{.} of the 2d International Workshop on Numerical and
  Symbolic Abstract Domains (NSAD'10)}, volume 267 of {\em Electronic Notes in
  Theoretical Computer Science (ENTCS)}. Elsevier, Sept{.} 2010.

\bibitem[MS12]{mine-SAS12}
A{.} Min{\'e} and D{.} Schmidt, editors.
\newblock {\em Proc{.} of the 19th International Static Analysis Symposium
  (SAS'12)}, volume 7460 of {\em Lecture Notes in Computer Science (LNCS)
  Advanced Research in Computing and Software Science (ARCoSS)}. Springer,
  Sept{.} 2012.

\bibitem[OM17]{mine-SAS17}
A{.} Ouadjaout and A{.} Min{\'e}.
\newblock Quantitative static analysis of communication protocols using
  abstract {M}arkov chains.
\newblock In {\em Proc{.}~of the 24st International Static Analysis Symposium
  (SAS'17)}, volume 10422 of {\em Lecture Notes in Computer Science (LNCS)},
  pages 277--29. Springer, Aug{.} 2017.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/article-ouadjaout-mine-sas17.pdf}.

\bibitem[OM19]{mine-FMSD19}
A{.} Ouadjaout and A{.} Min{\'e}.
\newblock Quantitative static analysis of communication protocols using
  abstract {M}arkov chains.
\newblock {\em Formal Methods in System Design (FMSD)}, 54(1):64--109, 2019.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/article-ouadjaout-al-fmsd19.pdf}.

\bibitem[OM20]{mine-SAS20}
A{.} Ouadjaout and A{.} Min{\'e}.
\newblock A library modeling language for the static analysis of {C} programs.
\newblock In {\em Proc{.}~of the 27th International Static Analysis Symposium
  (SAS'20)}, volume 12389 of {\em Lecture Notes in Computer Science (LNCS)},
  pages 223--246. Springer, Nov{.} 2020.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/ouadjaout-al-sas20.pdf}.

\bibitem[OMLB16]{mine-JSS16}
A{.} Ouadjaout, A{.} Min{\'e}, N{.} Lasla, and N{.} Badache.
\newblock Static analysis by abstract interpretation of functional properties
  of device drivers in {T}iny{O}{S}.
\newblock {\em Journal of Systems and Software (JSS)}, 120:114--132, 2016.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/article-ouadjaout-al-jss16.pdf}.

\bibitem[PM22]{mine-TASE22}
F{.} Parolini and A{.} Min{\'e}.
\newblock Sound static analysis of regular expressions for vulnerabilities to
  denial of service attacks.
\newblock In {\em Proc{.}~of the 16th International Symposium on Theoretical
  Aspects of Software Engineering (TASE'22)}, volume 13299 of {\em Lecture
  Notes in Computer Science (LNCS)}, pages 73--91. Springer, Jul{.} 2022.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/article-parolini-al-tase22.pdf}.

\bibitem[PM23]{mine-SCP23}
F{.} Parolini and A{.} Min{\'e}.
\newblock Sound static analysis of regular expressions for vulnerabilities to
  denial of service attacks (extended version).
\newblock {\em Science of Computer Programming (SCP)}, page~43, Jul{.} 2023.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/article-parolini-al-scp23.pdf}.

\bibitem[PM24]{mine-VMCAI24a}
F{.} Parolini and A{.} Min{\'e}.
\newblock Sound abstract nonexploitability analysis.
\newblock In {\em Proc{.}~of the 25th International Conference on Verification,
  Model Checking, and Abstract Interpretation (VMCAI'24)}, volume 14499 of {\em
  Lecture Notes in Computer Science (LNCS)}. Springer, Jan{.} 2024.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/article-parolini-al-vmcai24.pdf}.

\bibitem[PMTB13a]{mine-VMCAI13}
M{.} Pelleau, A{.} Min{\'e}, C{.} Truchet, and F{.} Benhamou.
\newblock A constraint solver based on abstract domains.
\newblock In {\em Proc{.}~of the 14th International Conference on Verification,
  Model Checking, and Abstract Interpretation (VMCAI'13)}, volume 7737 of {\em
  Lecture Notes in Computer Science (LNCS)}, pages 434--454. Springer, 20-22
  Jan{.} 2013.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/article-pelleau-vmcai2013.pdf}.

\bibitem[PMTB13b]{mine-JFPC13}
M{.} Pelleau, A{.} Min{\'e}, C{.} Truchet, and F{.} Benhamou.
\newblock Un solveur de contraintes bas{\'e} sur les domaines abstraits.
\newblock In {\em Proc{.}~of 9{\`e}mes Journ{\'e}es Francophones de
  Programmation par Contraintes (JFPC'13)}, pages 259--268, 12--13 Jun{.} 2013.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/article-pelleau-jfpc2013.pdf}.

\bibitem[SM16]{mine-SAS16a}
T{.} Suzanne and A{.} Min{\'e}.
\newblock From array domains to abstract interpretation under
  store-buffer-based memory models.
\newblock In {\em Proc{.}~of the 23st International Static Analysis Symposium
  (SAS'16)}, volume 9837 of {\em Lecture Notes in Computer Science (LNCS)},
  pages 469--488. Springer, Sep{.} 2016.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/article-suzanne-al-sas16.pdf}.

\bibitem[SM18]{mine-APLAS18}
T{.} Suzanne and A{.} Min{\'e}.
\newblock Relational thread-modular abstract interpretation under relaxed
  memory models.
\newblock In {\em Proc{.}~of the 16th Asian Symposium on Programming Languages
  and Systems (APLAS'18)}, volume 11275 of {\em Lecture Notes in Computer
  Science (LNCS)}, pages 109--128. Springer, Dec{.} 2018.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/suzanne-mine-aplas18.pdf}.

\bibitem[SMM{\etalchar{+}}23a]{mine-HIPEAC23}
N{.}~R{.} Shah, A{.} Misra, A{.} Min{\'e}, R{.} Venkat, and R{.} Upadrasta.
\newblock Scalable and accurate approximation framework for cache miss
  calculation.
\newblock In {\em Proc{.}~of HiPEAC (HiPEAC'23)}. ACM, Jan{.} 2023.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/shah-et-al-taco23.pdf}.

\bibitem[SMM{\etalchar{+}}23b]{mine-TACO23}
N{.}~R{.} Shah, A{.} Misra, A{.} Min{\'e}, R{.} Venkat, and R{.} Upadrasta.
\newblock Scalable and accurate approximation framework for cache miss
  calculation.
\newblock {\em ACM Transactions on Architecture and Code Optimization (TACO)},
  20(2):1--28, Mar{.} 2023.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/shah-et-al-taco23.pdf}.

\bibitem[UM14a]{mine-ESOP14}
C{.} Urban and A{.} Min{\'e}.
\newblock An abstract domain to infer ordinal-valued ranking functions.
\newblock In {\em Proc{.}~of the 23rd European Symposium on Programming
  (ESOP'14)}, volume 8410 of {\em Lecture Notes in Computer Science (LNCS)},
  pages 412--431. Springer, Apr{.} 2014.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/article-urban-mine-esop14.pdf}.

\bibitem[UM14b]{mine-SAS14a}
C{.} Urban and A{.} Min{\'e}.
\newblock A decision tree abstract domain for proving conditional termination.
\newblock In {\em Proc{.}~of the 21st International Static Analysis Symposium
  (SAS'14)}, volume 8373 of {\em Lecture Notes in Computer Science (LNCS)},
  pages 302--318. Springer, Sep{.} 2014.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/article-urban-mine-sas14.pdf}.

\bibitem[UM14c]{mine-WST14}
C{.} Urban and A{.} Min{\'e}.
\newblock To {I}nfinity{.}{.}{.} and {B}eyond!
\newblock In {\em Proc{.}~of the 14th International Workshop on Termination
  (WST'14)}, pages 85--89. Informal proceedings, Jul{.} 2014.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/article-urban-mine-wst14.pdf}.

\bibitem[UM15a]{mine-COMLAN15}
C{.} Urban and A{.} Min{\'e}.
\newblock Inference of ranking functions for proving temporal properties by
  abstract interpretation.
\newblock {\em Computer Languages, Systems and Structures (COMLAN)}, page~46,
  2015.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/article-urban-mine-comlan2015.pdf}.

\bibitem[UM15b]{mine-VMCAI15a}
C{.} Urban and A{.} Min{\'e}.
\newblock Proving guarantee and recurrence temporal properties by abstract
  interpretation.
\newblock In {\em Proc{.}~of the 16th International Conference on Verification,
  Model Checking, and Abstract Interpretation (VMCAI'15)}, volume 8931 of {\em
  Lecture Notes in Computer Science (LNCS)}, pages 190--208. Springer, Jan{.}
  2015.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/article-urban-mine-vmcai15.pdf}.

\bibitem[UM21]{mine-MLFM21}
C{.} Urban and A{.} Min{\'e}.
\newblock A review of formal methods applied to machine {L}earning.
\newblock Technical report, Computing Research Repository (arXiv) (CoRR),
  Apr{.} 2021.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/article-urban-mine-mlfm2021.pdf}.

\bibitem[VMM23]{mine-JFLA23}
M{.} Valnet, R{.} Monat, and A{.} Min{\'e}.
\newblock Analyse statique de valeurs par interpr{\'e}tation abstraite de
  programmes fonctionnels manipulant des types alg{\'e}briques r{\'e}cursifs.
\newblock In {\em Proc{.}~of Journ{\'e}es Francophones des Langages Applicatifs
  (JFLA'23)}, 31 Jan{.}--3 Feb{.} 2023.
\newblock
  \url{http://www-apr.lip6.fr/~mine/publi/article-valnet-al-jfla23.pdf}.

\bibitem[WCM{\etalchar{+}}15]{mine-EMSOFT15b}
W{.} Wu, L{.} Chen, A{.} Min{\'e}, D{.} Dong, and J{.} Wang.
\newblock Numerical static analysis of interrupt-driven programs via
  sequentialization.
\newblock In {\em Proc{.}~of the 15th International Conference on Embedded
  Software (EMSOFT'15)}, pages 55--64. IEEE CS Press, Oct{.} 2015.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-wu-al-emsoft15.pdf}.

\bibitem[WCM{\etalchar{+}}16]{mine-TECS16}
W{.} Wu, L{.} Chen, A{.} Min{\'e}, D{.} Dong, and J{.} Wang.
\newblock Numerical static analysis of interrupt-driven programs via
  sequentialization.
\newblock {\em ACM Transactions on Embedded Computing Systems (TECS)},
  15(70):26, Aug{.} 2016.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-wu-al-tecs16.pdf}.

\bibitem[ZMP{\etalchar{+}}19]{mine-NSAD19}
G{.} Ziat, A{.} Mar{\'e}chal, M{.} Pelleau, A{.} Min{\'e}, and C{.} Truchet.
\newblock Combination of boxes and polyhedra abstractions for constraint
  solving.
\newblock In {\em Proc{.}~of the 8th International Workshop on Numerical and
  Symbolic Abstract Domains (NSAD'19)}, number 1906, page~18. EasyChair
  Preprints, 8 Oct{.} 2019.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/preprint-ziat-al-nsad19.pdf}.

\bibitem[ZPTM18]{mine-CP18}
G{.} Ziat, M{.} Pelleau, C{.} Truchet, and A{.} Min{\'e}.
\newblock Finding solutions by finding inconsistencies.
\newblock In {\em Proc{.}~of the International Conference on Principles and
  Practice of Constraint Programming (CP'18)}, volume 11008 of {\em Lecture
  Notes in Computer Science (LNCS)}, pages 420--435. Springer, Aug{.} 2018.
\newblock \url{http://www-apr.lip6.fr/~mine/publi/article-pelleau-al-cp18.pdf}.

\end{thebibliography}