\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[MM24a]{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[MM24b]{mine-SAS24} M{.} Milanese and A{.} Min{\'e}. \newblock Under-approximating memory abstractions. \newblock In {\em Proc{.}~of the 31th International Static Analysis Symposium (SAS'24)}, volume 14995 of {\em Lecture Notes in Computer Science (LNCS)}. Springer, Oct{.} 2024. \newblock \url{http://www-apr.lip6.fr/~mine/publi/article-milanese-al-sas24.pdf}. \bibitem[MMP{\etalchar{+}}24]{mine-TACAS24} R{.} Monat, M{.} Milanese, F{.} Parolini, J{.} Boillot, A{.} Ouadjaout, and A{.} Min{\'e}. \newblock Mopsa-{C}: {I}mproved verification for {C} programs, simple validation of correctness witnesses (competition contribution). \newblock In {\em Proc{.}~of the 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'24)}, volume 14572 of {\em Lecture Notes in Computer Science (LNCS)}, pages 387--392. Springer, Apr{.} 2024. \newblock \url{http://www-apr.lip6.fr/~mine/publi/article-monat-al-tacas24.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[MOM23]{mine-TACAS23} R{.} Monat, A{.} Ouadjaout, and A{.} Min{\'e}. \newblock Mopsa-{C}: {M}odular domains and relational abstract interpretation for {C} programs (competition contribution). \newblock In {\em Proc{.}~of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'23)}, volume 13994 of {\em Lecture Notes in Computer Science (LNCS)}, pages 565--570. Springer, Apr{.} 2023. \newblock \url{http://www-apr.lip6.fr/~mine/publi/article-monat-al-tacas23.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[MRUM24]{mine-LPAR24} N{.} Moussaoui~Remil, C{.} Urban, and A{.} Min{\'e}. \newblock Automatic detection of vulnerable variables for {C}{T}{L} properties of programs. \newblock In {\em Proc{.}~of the 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'24)}, volume 100 of {\em EPiC Series in Computing}, pages 116--126. EasyChair Proceedings in Computing, May 2024. \newblock \url{http://www-apr.lip6.fr/~mine/publi/article-moussaoui-al-lpar24.pdf}. \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[RBM{\etalchar{+}}24]{mine-JFLA24} M{.} Razafintsialonina, D{.} B{\"u}hler, A{.} Min{\'e}, V{.} Perrelle, and J{.} Signoles. \newblock R{\'e}utilisations de caches et d'invariants pour l'analyse statique incr{\'e}mentale. \newblock In {\em Proc{.}~of Journ{\'e}es Francophones des Langages Applicatifs (JFLA'24)}, 30 Jan{.}--2 Feb{.} 2024. \newblock \url{http://www-apr.lip6.fr/~mine/publi/article-mamy-al-jfla24.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}