E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini, Cost Analysis of Java Bytecode, Proc. of the 16th European Symposium on Programming, pp.157-172, 2007.
DOI : 10.1007/978-3-540-71316-6_12

G. Amato and F. Scozzari, The Abstract Domain of Parallelotopes, Proceedings of the Fourth International Workshop on Numerical and Symbolic Abstract Domains, pp.17-28, 2012.
DOI : 10.1016/j.entcs.2012.09.003

C. Ancourt, F. Coelho, and F. Irigoin, A Modular Static Analysis Approach to Affine Loop Invariants Detection, Proceeding of the Second International Workshop on Numerical and Symbolic Abstract Domains: NSAD 2010, pp.3-16, 2010.
DOI : 10.1016/j.entcs.2010.09.002
URL : https://hal.archives-ouvertes.fr/hal-00586338

R. Bagnara, E. Ricci, E. Zaffanella, and P. M. Hill, Possibly Not Closed Convex Polyhedra and the Parma Polyhedra Library, Static Analysis: Proceedings of the 9th International Symposium, pp.213-229, 2002.
DOI : 10.1007/3-540-45789-5_17
URL : http://www.cs.unipr.it/~bagnara/Papers/PostScript/600dpi/Q286-600DPI.ps.gz

R. Bagnara, P. M. Hill, and E. Zaffanella, Widening operators for powerset domains, Proc. of the 5h Int. Conf. on Verification, Model Checking, and Abstract Interpretation, pp.135-148, 2004.
DOI : 10.1007/s10009-007-0029-y
URL : http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ03b.pdf

R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella, Precise widening operators for convex polyhedra, Science of Computer Programming, vol.58, issue.1-2, pp.28-56, 2005.
DOI : 10.1016/j.scico.2005.02.003
URL : https://doi.org/10.1016/j.scico.2005.02.003

R. Bagnara, E. Rodríguez-carbonell, and E. Zaffanella, Generation of Basic Semi-algebraic Invariants Using Convex Polyhedra, Static Analysis: 12th International Symposium, SAS 2005, pp.19-34, 2005.
DOI : 10.1007/11547662_4

R. Bagnara, P. M. Hill, and E. Zaffanella, An Improved Tight Closure Algorithm for Integer Octagonal Constraints, Verification, Model Checking and Abstract Interpretation: Proceedings of the 9th International Conference, pp.8-21, 2008.
DOI : 10.1007/978-3-540-78163-9_6
URL : http://www.cs.unipr.it/~bagnara/Papers/PDF/VMCAI08.pdf

R. Bagnara, P. M. Hill, and E. Zaffanella, The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems, Science of Computer Programming, vol.72, issue.1-2, pp.3-21, 2008.
DOI : 10.1016/j.scico.2007.08.001

R. Bagnara, P. M. Hill, and E. Zaffanella, Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness. Formal Methods in System Design, pp.279-323, 2009.

R. Bagnara, P. M. Hill, and E. Zaffanella, Exact join detection for convex polyhedra and other numerical abstractions, Computational Geometry, vol.43, issue.5, pp.453-473, 2010.
DOI : 10.1016/j.comgeo.2009.09.002
URL : https://doi.org/10.1016/j.comgeo.2009.09.002

G. Balakrishnan and T. Reps, Analyzing memory accesses in x86 executables, Proc. of the Int. Conf. on Compiler Construction number 2985 in LNCS, pp.5-23, 2004.
DOI : 10.21236/ada449077
URL : http://www.cs.wisc.edu/wpis/papers/tr1486r.ps

V. Balasundaram and K. Kennedy, A technique for summarizing data access and its use in parallelism enhancing transformations, ACM PLDI'89, pp.41-53, 1989.

F. Banterle and R. Giacobazzi, A Fast Implementation of the Octagon Abstract Domain on Graphics Hardware, Static Analysis: 14th International Symposium, SAS 2007 Proceedings, pp.315-332, 2007.
DOI : 10.1007/978-3-540-74061-2_20

C. Bartzis and T. Bultan, Efficient Symbolic Representations for Arithmetic Constraints in Verification, International Journal of Foundations of Computer Science, vol.1443, issue.04, pp.605-624, 2003.
DOI : 10.1023/A:1008678014487

C. Bartzis and T. Bultan, Widening Arithmetic Automata, Computer Aided Verification, 16th International Conference, CAV, pp.321-333, 2004.
DOI : 10.1007/978-3-540-27813-9_25
URL : http://www.cs.cmu.edu/~cbartzis/papers/widening.pdf

F. Benhamou, F. Goualard, L. Granvilliers, and J. Puget, Revisiting hull and box consistency, Proc. of the 16th Int. Conf. on Logic Programming, pp.230-244, 1999.

F. Benoy, A. King, and F. Mesnard, Computing convex hulls with a linear solver, Theory and Practice of Logic Programming, vol.5, issue.1-2, pp.259-271, 2005.
DOI : 10.1017/S1471068404002261

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development, 2004.
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237

J. Bertrane, P. Cousot, R. Cousot, J. Feret, L. Mauborgne et al., Static analysis and verification of aerospace software by abstract interpretation, AIAA Infotech@Aerospace, number 2010-3385 in AIAA, pp.1-38, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00528611

J. Bertrane, P. Cousot, R. Cousot, J. Feret, L. Mauborgne et al., Static analysis and verification of aerospace software by abstract interpretation, Foundations and Trends in Programming Languages (FnTPL), vol.2, pp.2-371, 2015.
URL : https://hal.archives-ouvertes.fr/inria-00528611

G. Birkhoff, Lattice theory, Colloquium Publications, 1967.
DOI : 10.1090/coll/025

B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne et al., A static analyzer for large safety-critical software, Proc. of the ACM SIGPLAN Conf. on Programming Languages Design and Implementation (PLDI'03), pp.196-207, 2003.
DOI : 10.1145/781151.781153
URL : https://hal.archives-ouvertes.fr/hal-00128135

M. Bouaziz, TreeKs: A Functor to Make Numerical Abstract Domains Scalable, 4th International Workshop on Numerical and Symbolic Abstract Domains, pp.41-52, 2012.
DOI : 10.1016/j.entcs.2012.09.005
URL : https://doi.org/10.1016/j.entcs.2012.09.005

F. Bourdoncle, Abstract, Journal of Functional Programming, vol.154, issue.04, pp.407-423, 1992.
DOI : 10.1007/978-3-642-67678-9

F. Bourdoncle, Abstract debugging of higher-order imperative languages, ACM SIGPLAN Notices, vol.28, issue.6, pp.46-55, 1993.
DOI : 10.1145/173262.155095

F. Bourdoncle, Efficient chaotic iteration strategies with widenings, Proc. of the Int. Conf. on Formal Methods in Programming and their Applications (FMPA'93), pp.128-141, 1993.
DOI : 10.1007/BFb0039704
URL : http://www.exentis.com/Francois.Bourdoncle/fmpa93.ps.Z

R. E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, vol.35, issue.8, pp.677-691, 1986.
DOI : 10.1109/TC.1986.1676819
URL : http://www.paradise.caltech.edu/cns188/Handouts/Bryant86.pdf

R. M. Burstall, Program proving as hand simulation with a little induction, Information Processing, pp.308-312, 1974.

L. Chen, A. Miné, and P. Cousot, A Sound Floating-Point Polyhedra Abstract Domain, Proc. of the Sixth Asian Symp. on Programming Languages and Systems (APLAS'08), pp.3-18, 2008.
DOI : 10.1007/3-540-45013-0_7
URL : https://hal.archives-ouvertes.fr/hal-00531567

L. Chen, A. Miné, J. Wang, and P. Cousot, Linear Absolute Value Relation Analysis, Proc. of the 20th European Symp. on Programming, pp.156-175, 2011.
DOI : 10.1007/3-540-45013-0_7
URL : https://hal.archives-ouvertes.fr/hal-00648039

N. V. Chernikova, Algorithm for discovering the set of all the solutions of a linear programming problem, USSR Computational Mathematics and Mathematical Physics, vol.8, issue.6, pp.282-293, 1968.
DOI : 10.1016/0041-5553(68)90115-8

C. K. Chiu and J. H. Lee, Efficient interval linear equality solving in constraint logic programming, Reliable Computing, vol.8, issue.2, pp.139-174, 2002.
DOI : 10.1023/A:1014754106275

E. Clarke, E. Emerson, and A. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems, vol.8, issue.2, pp.244-263, 1986.
DOI : 10.1145/5397.5399

E. Clarke, D. Kroening, and F. Lerda, A Tool for Checking ANSI-C Programs, Tools and Algorithms for the Construction and Analysis of Systems, pp.168-176, 2004.
DOI : 10.1007/978-3-540-24730-2_15

T. Cormen, C. Leiserson, R. Rivest, and C. Stein, Introduction to Algorithms, 2001.

A. Cortesi and M. Zanioli, Widening and narrowing operators for abstract interpretation, Computer Languages, Systems & Structures, vol.37, issue.1, pp.24-42, 2011.
DOI : 10.1016/j.cl.2010.09.001
URL : http://www.dsi.unive.it/~cortesi/paperi/compLang_2011.pdf

A. Cortesi, G. Filé, F. Ranzato, R. Giacobazzi, and C. Palamidessi, Complementation in abstract interpretation, ACM Transactions on Programming Languages and Systems, vol.19, issue.1, pp.7-47, 1997.
DOI : 10.1145/239912.239914
URL : http://www.math.unipd.it/%7Eranzato/papers/sas95.pdf

A. Cortesi, G. Costantini, and P. Ferrara, A Survey on Product Operators in Abstract Interpretation, Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday, pp.325-336, 2013.
DOI : 10.1007/978-3-540-31987-0_2

A. Costan, S. Gaubert, E. Goubault, M. Martel, and S. Putot, A Policy Iteration Algorithm for Computing Fixed Points in Static Analysis of Programs, Computer Aided Verification: 17th International Conference, CAV 2005, pp.462-475, 2005.
DOI : 10.1007/11513988_46

P. Cousot, Asynchronous iterative methods for solving a fixed point system of monotone equations in a complete lattice, Res. rep. R.R. Laboratoire IMAG, vol.88, issue.15, 1977.

P. Cousot, Semantic foundations of program analysis In Program Flow Analysis: Theory and Applications, chapter 10, pp.303-342, 1981.

P. Cousot, Types as abstract interpretations, invited paper, Conference Record of the Twentyfourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.316-331, 1997.

P. Cousot, Constructive design of a hierarchy of semantics of a transition system by abstract interpretation, Theoretical Computer Science, vol.277, issue.1-2, pp.47-103, 2002.
DOI : 10.1016/S0304-3975(00)00313-3

P. Cousot, Abstracting Induction by Extrapolation and Interpolation, Verification, Model Checking, and Abstract Interpretation: 16th International Conference, VMCAI 2015, pp.19-42, 2015.
DOI : 10.1007/978-3-662-46081-8_2

P. Cousot and R. Cousot, Static determination of dynamic properties of programs, Proc. of the 2d Int. Symp. on Programming, pp.106-130, 1976.

P. Cousot and R. Cousot, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, pp.238-252
DOI : 10.1145/512950.512973
URL : https://hal.archives-ouvertes.fr/hal-01108790

P. Cousot and R. Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '79, pp.269-282, 1979.
DOI : 10.1145/567752.567778

P. Cousot and R. Cousot, Constructive versions of Tarski???s fixed point theorems, Pacific Journal of Mathematics, vol.82, issue.1, pp.43-57, 1979.
DOI : 10.2140/pjm.1979.82.43

P. Cousot and R. Cousot, Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, invited paper, Proc. of the Int. Workshop on Programming Language Implementation and Logic Programming (PLILP'92), pp.269-295, 1992.
DOI : 10.1007/3-540-55844-6_142
URL : http://www.ens.fr/~cousot/publications.www/CousotCousot-PLILP-92-LNCS-n631-p269--295-1992.ps.gz

P. Cousot and R. Cousot, Abstract Interpretation Frameworks, Journal of Logic and Computation, vol.2, issue.4, pp.511-547, 1992.
DOI : 10.1093/logcom/2.4.511

P. Cousot and R. Cousot, ???A la Burstall??? intermittent assertions induction principles for proving inevitability properties of programs, Theoretical Computer Science, vol.120, issue.1, pp.123-155, 1993.
DOI : 10.1016/0304-3975(93)90248-R

P. Cousot and R. Cousot, A gentle introduction to formal verification of computer systems by abstract interpretation, Logics and Languages for Reliability and Security, NATO Science Series III: Computer and Systems Sciences, pp.1-29, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00543886

P. Cousot and N. Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '78, pp.84-97, 1978.
DOI : 10.1145/512760.512770

P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné et al., Combination of Abstractions in the ASTR??E Static Analyzer, Proc. of the 11th Annual Asian Computing Science Conf. (ASIAN'06), pp.272-300, 2006.
DOI : 10.1007/978-3-540-24725-8_2

P. Cousot, R. Cousot, and L. Mauborgne, A Scalable Segmented Decision Tree Abstract Domain, Pnueli Festschrift, pp.72-95, 2010.
DOI : 10.1007/3-540-61739-6_53
URL : https://hal.archives-ouvertes.fr/inria-00543632

R. Cousot, Reasoning about program invariance proof methods. Res. rep. CRIN-80-P050, Centre de Recherche en Informatique de Nancy (CRIN), Institut National Polytechnique de Lorraine, 1980.

P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles et al., Frama-C, Proc. of the 10th International Conference on Software Engineering and Formal Methods, SEFM'12, pp.233-247, 2012.
DOI : 10.1007/978-3-642-33826-7_16

E. W. Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, Communications of the ACM, vol.18, issue.8, pp.453-457, 1975.
DOI : 10.1145/360933.360975

N. Dor, M. Rodeh, and M. Sagiv, Cleanness Checking of String Manipulations in C Programs via Integer Analysis, Static Analysis: 8th International Symposium Proceedings, pp.194-212, 2001.
DOI : 10.1007/3-540-47764-0_12

J. Feret, Static Analysis of Digital Filters, Proc. of the 13th European Symp. on Programming, pp.33-48, 2004.
DOI : 10.1007/978-3-540-24725-8_4
URL : https://hal.archives-ouvertes.fr/inria-00528447

J. Feret, The Arithmetic-Geometric Progression Abstract Domain, Proc. of the 6th Int. Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI'05), pp.42-58, 2005.
DOI : 10.1007/978-3-540-30579-8_3
URL : https://hal.archives-ouvertes.fr/inria-00528450

G. Filé and F. Ranzato, The powerset operator on abstract interpretations, Theoretical Computer Science, vol.222, issue.1-2, pp.77-111, 1999.
DOI : 10.1016/S0304-3975(98)00007-3

R. W. Floyd, Assigning meanings to programs, Proc. of the American Mathematical Society Symposia on Applied Mathematics, pp.19-32, 1967.
DOI : 10.1090/psapm/019/0235771

G. Gange, J. A. Navas, P. Schachte, H. Søndergaard, and P. J. Stuckey, Interval Analysis and Machine Arithmetic, ACM Transactions on Programming Languages and Systems, vol.37, issue.1, pp.1-135, 2015.
DOI : 10.3233/JCS-2011-0434
URL : http://dl.acm.org/ft_gateway.cfm?id=2651360&type=pdf

K. Ghorbal, E. Goubault, and S. Putot, The Zonotope Abstract Domain Taylor1+, Proc. of the 21st Int. Conf. on Computer Aided Verification (CAV'09), pp.627-633, 2009.
DOI : 10.1137/050622870

R. Giacobazzi and F. Ranzato, Refining and compressing abstract domains, Automata, Languages and Programming: 24th International Colloquium, ICALP '97, pp.771-781, 1997.
DOI : 10.1007/3-540-63165-8_230
URL : http://profs.sci.univr.it/~giaco/download/icalp97.ps.gz

R. Giacobazzi and F. Ranzato, Optimal domains for disjunctive abstract interpretation, Science of Computer Programming, vol.32, issue.1-3, pp.177-210, 1998.
DOI : 10.1016/S0167-6423(97)00034-8
URL : https://doi.org/10.1016/s0167-6423(97)00034-8

R. Giacobazzi and F. Scozzari, A logical model for relational abstract domains, ACM Transactions on Programming Languages and Systems, vol.20, issue.5, pp.1067-1109, 1998.
DOI : 10.1145/293677.293680

R. Giacobazzi, F. Ranzato, and F. Scozzari, Making abstract interpretations complete, Journal of the ACM, vol.47, issue.2, pp.361-416, 2000.
DOI : 10.1145/333979.333989

P. Granger, Static analysis of arithmetical congruences, International Journal of Computer Mathematics, vol.30, issue.3-4, pp.165-199, 1989.
DOI : 10.1145/29873.29875

P. Granger, Static analysis of linear congruence equalities among variables of a program, Proc. of the Int. Joint Conf. on Theory and Practice of Soft. Development (TAP- SOFT'91), pp.169-192, 1991.
DOI : 10.1007/3-540-53982-4_10

P. Granger, Improving the results of static analyses of programs by local decreasing iterations, Foundations of Software Technology and Theoretical Computer Science: 12th Conference, pp.68-79, 1992.
DOI : 10.1007/3-540-56287-7_95

P. Granger, Static analyses of congruence properties on rational numbers (extended abstract), Static Analysis: 4th International Symposium, SAS '97, pp.278-292, 1997.
DOI : 10.1007/BFb0032748

N. Halbwachs and J. Henry, When the Decreasing Sequence Fails, Static Analysis: 19th International Symposium, SAS 2012, pp.198-213, 2012.
DOI : 10.1007/978-3-642-33125-1_15
URL : https://hal.archives-ouvertes.fr/hal-00734340

M. Handjieva and S. Tzolovski, Refining Static Analyses by Trace-Based Partitioning Using Control Flow, Static Analysis: 5th International Symposium, SAS'98, pp.200-214, 1998.
DOI : 10.1007/3-540-49727-7_12

C. A. Hoare, An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-580, 1969.
DOI : 10.1145/363235.363259
URL : http://www.utdallas.edu/~kxh060100/cs6371fa07/hoare.pdf

B. Jeannet, Dynamic partitioning in linear relation analysis: Application to the verification of reactive systems, Formal Methods in System Design, vol.23, issue.1, pp.5-37, 2003.
DOI : 10.1023/A:1024480913162

B. Jeannet and A. Miné, Apron: A Library of Numerical Abstract Domains for Static Analysis
DOI : 10.1007/3-540-45013-0_7
URL : https://hal.archives-ouvertes.fr/hal-00786354

G. Kahn, Natural semantics, 1987.
DOI : 10.1007/BFb0039592
URL : https://hal.archives-ouvertes.fr/inria-00075953

M. Karr, Affine relationships among variables of a program, Acta Informatica, vol.6, issue.2, pp.133-151, 1976.
DOI : 10.1007/BF00268497

J. C. King, Symbolic execution and program testing, Communications of the ACM, vol.19, issue.7, pp.385-394, 1976.
DOI : 10.1145/360248.360252

S. C. Kleene, Introduction to metamathematics. Bibliotheca mathematica, 1964.

S. Lang, Introduction to Linear Algebra, Undergraduate Texts in Mathematics, 1997.
DOI : 10.1007/978-1-4612-1070-2

H. Leverge, A note on Chernikova's algorithm, 1992.

F. Logozzo and M. Fähndrich, Pentagons, Proceedings of the 2008 ACM symposium on Applied computing , SAC '08, pp.796-807, 2010.
DOI : 10.1145/1363686.1363736

A. Maréchal, D. Monniaux, and M. Périn, Scalable Minimizing-Operators on Polyhedra via Parametric Linear Programming, Static Analysis -24th International Symposium, pp.212-231, 2017.
DOI : 10.1145/2737924.2738000

I. Mastroeni, Algebraic power analysis by abstract interpretation. Higher-Order and Symbolic Computation, pp.297-345, 2004.
DOI : 10.1007/s10990-004-4867-y
URL : http://profs.sci.univr.it/~mastroen/download/hoscPower.pdf

L. Mauborgne and X. , Trace Partitioning in Abstract Interpretation Based Static Analyzers, Proc. of the 14th European Symp. on Programming (ESOP'05), pp.5-20, 2005.
DOI : 10.1007/978-3-540-31987-0_2

K. Mcmillan, Symbolic Model Checking, Kluwer, 1993.

A. Miné, A New Numerical Abstract Domain Based on Difference-Bound Matrices, Proc. of the Second Symposium on Programs as Data Objects (PADO II), pp.155-172, 2001.
DOI : 10.1007/3-540-44978-7_10

A. Miné, Relational Abstract Domains for the Detection of Floating-Point Run-Time Errors, Proc. of the European Symp. on Programming, pp.3-17, 2004.
DOI : 10.1007/978-3-540-24725-8_2

A. Miné, The octagon abstract domain. Higher-Order and Symbolic Computation, pp.31-100, 2006.

A. Miné, Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics, Proc. of the ACM SIGPLAN/SIGBED Conf. on Languages, Compilers, and Tools for Embedded Systems (LCTES'06), pp.54-63, 2006.

A. Miné, Abstract domains for bit-level machine integer and floating-point operations, Proc. of the 4th Int. Workshop on Invariant Generation (WING'12), number HW- MACS-TR-0097 in EPiC Series in Computing, p.16, 2012.

R. E. Moore, Interval Analysis, 1966.

M. Müller-olm and H. Seidl, Analysis of modular arithmetic, Proc. of the 14th European Symp. on Prog. (ESOP'05), pp.46-60, 2005.

D. Nguyen-que, Robust and generic abstract domain for static program analysis: The polyhedral case, 2010.

H. Oh, K. Heo, W. Lee, W. Lee, and K. Yi, Design and implementation of sparse global analyses for C-like languages, ACM SIGPLAN Notices, vol.47, issue.6, pp.229-238, 2012.
DOI : 10.1145/1041685.1029911

S. Owre, J. M. Rushby, and N. Shankar, PVS: A prototype verification system, Proc. of the 11th Int. Conf. on Automated Deduction (CADE'92), volume 607 of LNAI, pp.748-752, 1992.
DOI : 10.1007/3-540-55602-8_217
URL : http://www.csl.sri.com/papers/c/a/cade92-pvs/cade92-pvs.ps.gz

G. D. Plotkin, A structural approach to operational semantics, 1981.

W. Pugh, The Omega test: a fast and practical integer programming algorithm for dependence analysis, Proceedings of the 1991 ACM/IEEE conference on Supercomputing , Supercomputing '91, pp.4-13, 1992.
DOI : 10.1145/125826.125848

H. G. Rice, Classes of recursively enumerable sets and their decision problems, Transactions of the American Mathematical Society, vol.74, issue.2, pp.358-366, 1953.
DOI : 10.1090/S0002-9947-1953-0053041-6

E. Rodríguez-carbonell and D. Kapur, Automatic generation of polynomial invariants of bounded degree using abstract interpretation, Science of Computer Programming, vol.64, issue.1, pp.54-75, 2007.
DOI : 10.1016/j.scico.2006.03.003

S. Sankaranarayanan, H. Sipma, and Z. Manna, Scalable Analysis of Linear Systems Using Mathematical Programming, Proc. of the 6th Int. Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI'05), pp.21-47, 2005.
DOI : 10.1007/978-3-540-30579-8_2

D. Schmidt, Abstract Interpretation from a Topological Perspective, Static Analysis: 16th International Symposium, SAS 2009, pp.293-308, 2009.
DOI : 10.1007/BFb0036946
URL : http://www.cis.ksu.edu/santos/schmidt/sas09.pdf

P. Schrammel and B. Jeannet, Logico-Numerical Abstract Acceleration and Application to the Verification of Data-Flow Programs, Static Analysis: 18th International Symposium, SAS 2011, pp.233-248, 2011.
DOI : 10.1007/s10703-006-0031-0
URL : https://hal.archives-ouvertes.fr/inria-00596241

A. Schrijver, Theory of linear and integer programming, 1986.

D. Scott and C. Strachey, Towards a mathematical semantics for computer languages, 1971.

Y. Seladji, Finding Relevant Templates via the Principal Component Analysis, Verification , Model Checking, and Abstract Interpretation, VMCAI 2017, pp.483-499, 2017.
DOI : 10.1111/1467-9868.00196

A. Simon and A. King, Analyzing String Buffers in C, Proceedings of the 9th International Conference on Algebraic Methodology and Software Technology, AMAST '02, pp.365-379, 2002.
DOI : 10.1007/3-540-45719-4_25
URL : http://www.cs.ukc.ac.uk/pubs/2002/1367/content.ps

A. Simon and A. King, Exploiting Sparsity in Polyhedral Analysis, Proc. of the 12th Int. Symp. on Static Analysis (SAS'05), pp.336-351, 2005.
DOI : 10.1007/11547662_23
URL : http://kar.kent.ac.uk/37606/1/content.pdf

A. Simon and A. King, Taming the Wrapping of Integer Arithmetic, Proc. of the 14th Int. Symp. on Static Analysis (SAS'07), pp.121-136, 2007.
DOI : 10.1007/978-3-540-74061-2_8

A. Simon, A. King, and J. M. Howe, Two Variables per Linear Inequality as an Abstract Domain, Proc. of the 12th Int. Conf. on Logic based program synthesis and transformation (LOPSTR'02), volume 2664 of LNCS, pp.71-89, 2002.
DOI : 10.1007/3-540-45013-0_7
URL : http://www2.in.tum.de/bib/files/simon02two.pdf

G. Singh, M. Püschel, and M. Vechev, Fast polyhedra abstract domain, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pp.46-59, 2017.
DOI : 10.1145/3093333.3009885

A. Tarski, A lattice-theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics, vol.5, issue.2, pp.285-310, 1955.
DOI : 10.2140/pjm.1955.5.285

A. Turing, Checking a large routine, Report of a Conference on High Speed Automatic Calculating Machines, pp.67-69, 1949.

C. Urban and A. Miné, A Decision Tree Abstract Domain for Proving Conditional Termination, Proc. of the 21st International Static Analysis Symposium (SAS'14), pp.302-318, 2014.
DOI : 10.1007/978-3-319-10936-7_19
URL : https://hal.archives-ouvertes.fr/hal-01105221

A. Venet, A Scalable Nonuniform Pointer Analysis for Embedded Programs, Proc. of the Int. Symp. on Static Analysis number 3148 in LNCS, pp.149-164, 2004.
DOI : 10.1007/978-3-540-27864-1_13
URL : http://ase.arc.nasa.gov/docs/../people/venet/sas04.pdf