D. Avis, D. Bremner, and R. Seidel, How good are convex hull algorithms?, Computational Geometry, vol.7, issue.5-6, pp.265-301, 1997.
DOI : 10.1016/S0925-7721(96)00023-5

D. Avis and K. Fukuda, A pivoting algorithm for convex hulls and vertex enumeration of arrangements and polyhedra, Discrete & Computational Geometry, vol.8, issue.3, pp.295-313, 1992.
DOI : 10.1007/BF02293050

D. Avis and K. Fukuda, Reverse search for enumeration, Discrete Applied Mathematics, vol.65, issue.1-3, pp.21-46, 1996.
DOI : 10.1016/0166-218X(95)00026-N

[. Ausiello, P. G. Franciosa, and D. Frigioni, Directed Hypergraphs: Problems, Algorithmic Results, and a Novel Decremental Approach, Theoretical Computer Science, 7th Italian Conference, ICTCS 2001, Proceedings, volume 2202 of Lecture Notes in Computer Science, pp.312-327, 2001.
DOI : 10.1007/3-540-45446-2_20

G. Ausiello, P. G. Franciosa, D. Frigioni, and R. Giaccio, Decremental maintenance of reachability in hypergraphs and minimum models of horn formulae, Algorithms and Computation, 8th International Symposium, ISAAC '97 Proceedings, volume 1350 of Lecture Notes in Computer Science, pp.122-131, 1997.
DOI : 10.1007/3-540-63890-3_14

X. Allamigeon, S. Gaubert, and . Goubault, Inferring Min and Max Invariants Using Max-Plus Polyhedra, SAS'08, pp.189-204, 2008.
DOI : 10.1007/978-3-540-69166-2_13

M. Akian, S. Gaubert, and A. Guterman, Tropical polyhedra are equivalent to mean payoff games. preprint, 2009.
URL : https://hal.archives-ouvertes.fr/hal-00778078

S. Agg09b-]-xavier-allamigeon, E. Gaubert, and . Goubault, Computing the Extreme Points of Tropical Polyhedra. arXiv:math/0904, 2009.

S. Xavier-allamigeon, E. Gaubert, and . Goubault, The Tropical Double Description Method, Proceedings of the 27th International Symposium on Theoretical Aspects of Computer Science (STACS'10), 2010.

W. Xavier-allamigeon, C. Godard, and . Hymans, Static Analysis of String Manipulations in Critical Embedded C Programs, Static Analysis, 13th International Symposium (SAS'06), pp.35-51, 2006.
DOI : 10.1007/11823230_4

S. [. Akian, V. N. Gaubert, and . Kolokoltsov, Set coverings and invertibility of functional Galois connections, Idempotent Mathematics and Mathematical Physics, Contemporary Mathematics, pp.19-51, 2005.
DOI : 10.1090/conm/377/06983
URL : https://hal.archives-ouvertes.fr/inria-00000966

S. Xavier-allamigeon, R. D. Gaubert, and . Katz, The number of extreme points of tropical polyhedra, Journal of Combinatorial Theory, Series A, vol.118, issue.1, 2010.
DOI : 10.1016/j.jcta.2010.04.003

C. Xavier-allamigeon and . Hymans, Analyse Statique par Interprétation Abstraite : ApplicationàApplicationà la Détection de Dépassement de Tampon, ` eme Symposium sur la Sécurité des Technologies de l'Information et des Communications (SSTIC'07), pp.347-384, 2007.

C. Xavier-allamigeon and . Hymans, Static analysis by abstract interpretation: application to the detection of heap overflows, Journal in Computer Virology, vol.5, issue.3, pp.5-23, 2008.
DOI : 10.1007/s11416-007-0063-z

A. V. Aho, J. E. Hopcroft, and J. D. Ullman, Data Structures and Algorithms, 1983.

G. Ausiello and G. F. Italiano, On-line algorithms for polynomially solvable satisfiability problems, The Journal of Logic Programming, vol.10, issue.1, pp.69-90509, 1978.
DOI : 10.1016/0743-1066(91)90006-B

X. Allamigeon, Non-disjunctive Numerical Domain for Array Predicate Abstraction, Programming Languages and Systems , 17th European Symposium on Programming Proceedings, pp.163-177, 2008.
DOI : 10.1007/978-3-540-78739-6_14
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.592.1207

X. Allamigeon, TPLib: Tropical polyhedra library, 2009.
DOI : 10.1016/j.jcta.2013.01.011
URL : http://arxiv.org/abs/1205.6314

A. [. Butkovi? and . Aminu, Introduction to max-linear programming, IMA Journal of Management Mathematics, vol.20, issue.3, 2008.
DOI : 10.1093/imaman/dpn029

]. K. Bat68 and . Batcher, Sorting networks and their applications, Proceedings of the AFIPS Spring Joint Computer Conference 32, pp.307-314, 1968.

]. B. Bcc-+-03, P. Blanchet, R. Cousot, J. Cousot, L. Feret et al., A static analyzer for large safety-critical software, ACM SIGPLAN PLDI'03, pp.196-207, 2003.

J. Berdine, C. Calcagno, B. Cook, D. Distefano, O. Peter et al., Shape Analysis for Composite Data Structures, Proceedings of the 19th International Conference on Computer Aided Verification, 2007.
DOI : 10.1007/978-3-540-73368-3_22

J. Berdine, C. Calcagno, B. Cook, D. Distefano, O. Peter et al., Shape Analysis for Composite Data Structures, Proceedings of the 19th International Conference on Computer Aided Verification, 2007.
DOI : 10.1007/978-3-540-73368-3_22

G. [. Baccelli, G. J. Cohen, J. P. Olsder, and . Quadrat, Synchronization and Linearity, 1992.

G. [. Butkovi? and . Hegedüs, An elimination method for finding all solutions of the system of linear equations over an extremal algebra, Ekonomickomatematicky Obzor, vol.20, 1984.

C. [. Briec and . Horvath, B-convexity. Optimization, pp.103-127, 2004.

D. Beyer, T. A. Henzinger, R. Majumdar, and A. Rybalchenko, Path invariants, PLDI '07: Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, pp.300-309, 2007.

C. [. Briec, A. Horvath, and . Rubinov, Separation in B-convexity, Pacific Journal of Optimization, vol.1, pp.13-30, 2005.

P. [. Bagnara, E. Hill, E. Ricci, and . Zaffanella, Precise Widening Operators for Convex Polyhedra, Static Analysis: Proceedings of the 10th International Symposium Proceedings of the 18th International Conference on Computer Aided Verification, pp.337-354, 2003.
DOI : 10.1007/3-540-44898-5_19

P. [. Bagnara, E. Hill, and . Zaffanella, Widening operators for powerset domains. Software Tools for Technology Transfer, pp.449-466, 2006.

P. [. Bagnara, E. Hill, and . 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

[. Ball, R. Majumdar, T. Millstein, and S. K. Rajamani, Automatic predicate abstraction of C programs, ACM SIGPLAN Notices, vol.36, issue.5, pp.203-213, 2001.
DOI : 10.1145/381694.378846

[. Bezem, R. Nieuwenhuis, and E. Rodríguez, Exponential behaviour of the Butkovi?????Zimmermann algorithm for solving two-sided linear systems in max-algebra, Discrete Applied Mathematics, vol.156, issue.18, pp.3506-3509, 2008.
DOI : 10.1016/j.dam.2008.03.016

M. Bezem, R. Nieuwenhuis, and E. Rodríguez, The Max-Atom Problem and Its Relevance, Logic for Programming, Artificial Intelligence, and Reasoning , 15th International Conference, pp.47-61, 2008.
DOI : 10.1007/978-3-540-89439-1_4

H. [. Butkovi?, S. Schneider, and . Sergeev, Generators, extremals and bases of max cones, Linear Algebra and its Applications, vol.421, issue.2-3, pp.394-406, 2007.
DOI : 10.1016/j.laa.2006.10.004

P. Butkovic and K. Zimmermann, A strongly polynomial algorithm for solving two-sided linear systems in max-algebra, Discrete Applied Mathematics, vol.154, issue.3, pp.437-446, 2006.
DOI : 10.1016/j.dam.2005.09.008

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

R. [. Cousot and . 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. Cc92a, R. Cousot, and . Cousot, Abstract interpretation and application to logic programs, Journal of Logic Programming, vol.13, pp.2-3, 1992.

]. P. Cc92b, R. Cousot, and . Cousot, Abstract interpretation frameworks, Journal of Logic and Computation, vol.2, issue.4, pp.511-547, 1992.

R. Clarisó and J. Cortadella, The Octahedron Abstract Domain, Static Analysis Symposium (SAS), pp.312-327, 2004.
DOI : 10.1007/978-3-540-27864-1_23

P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné et al., The ASTRE?? Analyzer, Proceedings of the European Symposium on Programming (ESOP'05), pp.21-30, 2005.
DOI : 10.1007/978-3-540-31987-0_3

L. Christopher, D. Conway, K. S. Dams, C. Namjoshi, and . Barrett, Points-to analysis, conditional soundness, and proving the absence of errors, Static Analysis Symposium (SAS), pp.62-77, 2008.

E. [. Clarke, A. P. Emerson, and . 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

. [. Cuninghame-green, Projections in minimax algebra, Mathematical Programming, pp.111-123, 1976.
DOI : 10.1093/imamat/11.2.145

. [. Cuninghame-green, Minimax algebra, of Lecture Notes in Economics and Mathematical Systems, 1979.
DOI : 10.1007/978-3-642-48708-8

P. [. Cuninghame-green and . Butkovic, The equation A???x=B???y over (max,+), Theoretical Computer Science, vol.293, issue.1, pp.3-12, 2003.
DOI : 10.1016/S0304-3975(02)00228-1

E. M. Clarke, O. Grumberg, and D. E. Long, Model checking and abstraction, ACM Transactions on Programming Languages and Systems, vol.16, issue.5, pp.1512-1542, 1994.
DOI : 10.1145/186025.186051

. G. Cgmq, S. Cohen, M. Gaubert, J. Mcgettrick, and . Quadrat, Maxplus toolbox of scilab Available at http://minimal.inria.fr/gaubert/maxplustoolbox

S. [. Cohen, J. P. Gaubert, and . Quadrat, Max-plus algebra and system theory: Where we are and where to go now, Annual Reviews in Control, vol.23, pp.207-219, 1999.
DOI : 10.1016/S1367-5788(99)90091-3

S. [. Cohen, J. P. Gaubert, and . Quadrat, Hahn-Banach separation theorem for max-plus semimodules, Optimal Control and Partial Differential Equations, pp.325-334, 2001.

S. [. Cohen, J. P. Gaubert, and . Quadrat, Duality and separation theorems in idempotent semimodules, Linear Algebra and its Applications, vol.379, pp.395-422, 2004.
DOI : 10.1016/j.laa.2003.08.010
URL : https://hal.archives-ouvertes.fr/inria-00071917

G. Cohen, S. Gaubert, J. P. Quadrat, and I. Singer, Max-plus convex sets and functions, Idempotent Mathematics and Mathematical Physics, Contemporary Mathematics, pp.105-129, 2005.
DOI : 10.1090/conm/377/06987

N. [. Cousot and . 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

]. B. Cha93 and . Chazelle, An optimal convex hull algorithm in any fixed dimension. Discrete and Compututational Geometry, pp.377-409, 1993.

]. N. Che68 and . Chernikova, Algorithm for discovering the set of all solutions of a linear programming problem, U.S.S.R. Computational Mathematics and Mathematical Physics, vol.8, issue.6, pp.282-293, 1968.

[. Christof and A. Löbel, The porta library

[. Cheriyan and K. Mehlhorn, Algorithms for dense graphs and networks on the random access computer, Algorithmica, vol.1, issue.1, pp.521-549, 1996.
DOI : 10.1007/BF01940880

]. P. Cou03 and . Cousot, Verification by abstract interpretation, Proc. Int. Symp. on Verification ? Theory & Practice ? Honoring Zohar Manna's 64th Birthday, pp.243-268, 2003.

H. Thomas, C. Cormen, R. L. Stein, C. E. Rivest, and . Leiserson, Introduction to Algorithms, 2001.

]. G. Dan63 and . Dantzig, Linear Programming and Extensions, 1963.

]. A. Deu92 and . Deutsch, A storeless model of aliasing and its abstractions using finite representations of right-regular equivalence relations, ICCL'92, Proceedings of the 1992 International Conference on Computer Languages, pp.2-13, 1992.

A. Deutsch, Interprocedural may-alias analysis for pointers: beyond klimiting, PLDI '94: Proceedings of the ACM SIGPLAN 1994 conference on Programming language design and implementation, pp.230-241, 1994.
DOI : 10.1145/773473.178263

[. Loreto, S. Gaubert, R. D. Katz, and J. Loiseau, Duality Between Invariant Spaces for Max-Plus Linear Discrete Event Systems, SIAM Journal on Control and Optimization, vol.48, issue.8, 2009.
DOI : 10.1137/090747191
URL : https://hal.archives-ouvertes.fr/hal-00562586

[. Distefano, P. W. Hearn, and H. Yang, A Local Shape Analysis Based on Separation Logic, Tools and Algorithms for the Construction and Analysis of Systems, 12th International Conference, pp.287-302, 2006.
DOI : 10.1145/514188.514190

[. Dor, M. Rodeh, and M. Sagiv, Cssv: towards a realistic tool for statically detecting all buffer overflows in C, PLDI '03: Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, pp.155-167, 2003.

M. Develin and B. Sturmfels, Tropical convexity, Doc. Math, vol.9, pp.1-27, 2004.

J. [. Develin and . Yu, Tropical Polytopes and Cellular Resolutions, Experimental Mathematics, vol.16, issue.3, pp.277-292, 2007.
DOI : 10.1080/10586458.2007.10129009
URL : http://arxiv.org/abs/math/0605494

. Jr, . M. Edmund, and . Clarke, Orna Grumberg, and Doron A. Peled. Model checking, 1999.

W. Mark, J. A. Eichin, and . Rochlis, With microscope and tweezers: An analysis of the internet virus of november 1988, IEEE Symposium on, p.326, 1989.

]. Fil03 and . Filliâtre, Why: a multi-language multi-prover verification tool, Research Report, vol.1366, 2003.

J. Filliâtre, Implementation of hash sets for OCaml, 2008.

K. Fukuda and A. Prodon, Double description method revisited, Selected papers from the 8th Franco-Japanese and 4th Franco-Chinese Conference on Combinatorics and Computer Science, pp.91-111, 1996.
DOI : 10.1007/3-540-61576-8_77
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.45.8343

[. Flanagan and S. Qadeer, Predicate abstraction for software verification, POPL '02: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp.191-202, 2002.

]. K. Fuk and . Fukuda, The cdd library

N. Harold and . Gabow, Path-based depth-first search for strong and biconnected components, Inf. Process. Lett, vol.74, issue.3-4, pp.107-114, 2000.

[. Ganssle, Big Code, 2005.

]. S. Gau92 and . Gaubert, Théorie des systèmes linéaires dans les dio¨?desdio¨?des, Thèse, ´ Ecole des Mines de Paris, 1992.

S. Bhargav, S. Gulavani, and . Gulwani, A numerical abstract domain based on expression abstraction and max operator with application in timing analysis, Computer Aided Verification, 20th International Conference, pp.370-384, 2008.

G. Gallo, C. Gentile, D. Pretolani, and G. Rago, Max Horn SAT and the minimum cut problem in directed hypergraphs, Mathematical Programming, vol.1, issue.3, pp.213-237, 1998.
DOI : 10.1007/BF01581727

R. [. Gaubert and . Katz, Max-Plus Convex Geometry, Lecture Notes in Comput. Sci, vol.4136, pp.192-206, 2006.
DOI : 10.1007/11828563_13
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.217.7868

R. [. Gaubert and . Katz, The Minkowski theorem for max-plus convex sets, Linear Algebra and its Applications, vol.421, issue.2-3, pp.356-369, 2007.
DOI : 10.1016/j.laa.2006.09.019
URL : https://hal.archives-ouvertes.fr/inria-00071358

]. S. Gk09a, R. Gaubert, and . Katz, The tropical analogue of polar cones, Linear Algebra and Appl, vol.431, pp.608-625, 2009.

[. Gaubert and R. D. Katz, Minimal half-spaces and external representation of tropical polyhedra, Journal of Algebraic Combinatorics, vol.13, issue.2, 2009.
DOI : 10.1007/s10801-010-0246-4

G. Gallo, G. Longo, S. Pallottino, S. [. Nguyen, F. Gaubert et al., Directed hypergraphs and applications, Discrete Applied Mathematics, vol.42, issue.2-3, pp.177-201, 1993.
DOI : 10.1016/0166-218X(93)90045-P

[. Gulwani, B. Mccloskey, and A. Tiwari, Lifting abstract interpreters to quantified logical domains, POPL'08: Proceedings of the 35th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 2008.

M. [. Gaubert and . Plus, Methods and applications of (max,+) linear algebra, STACS'97 number 1200, 1997.
DOI : 10.1007/BFb0023465
URL : https://hal.archives-ouvertes.fr/inria-00073603

E. Goubault and S. Putot, Static Analysis of Numerical Algorithms, Static Analysis, 13th International Symposium (SAS'06), pp.18-5134, 2006.
DOI : 10.1007/11823230_3

F. [. Giacobazzi and . Ranzato, Optimal domains for disjunctive abstract interpretation, Science of Computer Programming, vol.32, issue.1-3, pp.1-3177, 1998.
DOI : 10.1016/S0167-6423(97)00034-8

P. Granger, Static analysis of linear congruence equalities among variables of a program, International Joint Conference on Theory and Practice of Software Development, pp.169-192, 1991.
DOI : 10.1007/3-540-53982-4_10

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

[. Gopan, A framework for numeric analysis of array operations, ACM SIGPLAN Notices, vol.40, issue.1, pp.338-350, 2005.
DOI : 10.1145/1047659.1040333

[. Gulwani and A. Tiwari, Combining abstract interpreters, PLDI '06: Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, pp.376-386, 2006.
DOI : 10.1145/1133255.1134026

]. N. Hal79 and . Halbwachs, Détermination Automatique de Relations Linéaires Vérifiées par les Variables d'un Programme, Thèse de 3 ` eme cycle d'informatique, 1979.

C. Hymans, O. Levillain, and . Newspeak, Doubleplussimple Minilang for Goodthinkful Static Analysis of C, 2008.

N. Halbwachs and M. Péron, Discovering properties about arrays in simple programs, Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, pp.339-348, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00288274

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

[. Jung, J. Kim, J. Shin, and K. Yi, Taming False Alarms from a Domain-Unaware C Analyzer by a Bayesian Statistical Post Analysis, Static Analysis: 12th International Symposium, SAS 2005. Proceedings, Lecture Notes in Computer Science, pp.203-217, 2005.
DOI : 10.1007/11547662_15

[. Jeannet and A. Miné, APRON numerical abstract domain library

[. Jhala and K. L. Mcmillan, Array Abstractions from Proofs, CAV, pp.193-206, 2007.
DOI : 10.1007/978-3-540-73368-3_23
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.83.8283

]. M. Jos05 and . Joswig, Tropical halfspaces, Combinatorial and computational geometry, pp.409-431, 2005.

M. Joswig, Tropical convex hull computations, 2008.
DOI : 10.1090/conm/495/09698
URL : http://arxiv.org/abs/0809.4694

J. R. Ghidella and J. Friedman, Streamlined development of body electronics systems using model-based design, 2006.

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

]. R. Kat07 and . Katz, Max-plus (A, B)-invariant spaces and control of timed discrete event systems, IEEE Trans. Aut. Control, vol.52, issue.2, pp.229-241, 2007.

L. Khachiyan, E. Boros, K. Borys, K. Elbassioni, and V. Gurvich, Generating all vertices of a polyhedron is hard, SODA '06: Proceedings of the seventeenth annual ACM-SIAM symposium on Discrete algorithm, pp.758-765, 2006.

A. Gary and . Kildall, A unified approach to global program optimization, POPL, pp.194-206, 1973.

. L. Llf-+-96-]-j, L. Lions, J. L. Lübeck, G. Fauquembergue, W. Kahn et al., Ariane 5, flight 501 failure, report by the inquiry board, 1996.

X. Liu and S. A. Smolka, Simple linear-time algorithms for minimal fixed points (extended abstract), Automata, Languages and Programming, 25th International Colloquium, ICALP'98, Proceedings, volume 1443 of Lecture Notes in Computer Science, pp.53-66, 1998.

[. Verge, A note on Chernikova's algorithm, 1992.

V. Maraia, The Build Master: Microsoft's Software Configuration Management Best Practices, 2005.

S. Mcconnell, Code Complete, Second Edition, 2004.

]. P. Mcm70 and . Mcmullen, The maximum numbers of faces of a convex polytope, Mathematika, vol.17, pp.179-184, 1970.

]. A. Min01a and . Miné, A new numerical abstract domain based on difference-bound matrices, PADO II, pp.155-172, 2001.

]. A. Min01b and . Miné, The octagon abstract domain, AST, pp.310-319, 2001.

]. A. Min04 and . Miné, Weakly Relational Numerical Abstract Domains, 2004.

]. A. Min06 and . Miné, Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics, ACM SIGPLAN LCTES'06, pp.54-63, 2006.

D. Monniaux, The pitfalls of verifying floating-point computations, ACM Transactions on Programming Languages and Systems, vol.30, issue.3, p.12, 2008.
DOI : 10.1145/1353445.1353446
URL : https://hal.archives-ouvertes.fr/hal-00128124

[. Müller-olm and H. Seidl, A Note on Karr???s Algorithm, Lecture Notes in Computer Science, vol.3142, pp.1016-1028, 2004.
DOI : 10.1007/978-3-540-27836-8_85

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

H. [. Motzkin, G. L. Raiffa, and R. M. Thompson, 3. The Double Description Method, Contributions to the Theory of Games, volume II, pp.51-73, 1953.
DOI : 10.1515/9781400881970-004

N. J. Nilsson, Problem-Solving Methods in Artificial Intelligence, 1971.

C. George, S. Necula, S. Mcpeak, W. Prakash-rahul, and . Weimer, CIL: Intermediate language and tools for analysis and transformation of C programs, CC '02: Proceedings of the 11th International Conference on Compiler Construction, pp.213-228, 2002.

G. Nelson and D. C. Oppen, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems, vol.1, issue.2, pp.245-257, 1979.
DOI : 10.1145/357073.357079

S. [. Nguyen and . Pallottino, Hyperpaths and shortest hyperpaths, COMO '86: Lectures given at the third session of the Centro Internazionale Matematico Estivo (C.I.M.E.) on Combinatorial optimization. [NPG98] Sang Nguyen, Stefano Pallottino, and Michel Gendreau. Implicit enumeration of hyperpaths in a logit model for transit networks, pp.258-27154, 1989.
DOI : 10.1007/BFb0083470

I. [. Nitica and . Singer, Max-plus convex sets and max-plus semispaces. I. Optimization, pp.171-205, 2007.
DOI : 10.1080/02331930600819852

C. Can and . Ozturan, On finding hypercycles in chemical reaction networks, Appl. Math. Lett, vol.21, issue.9, pp.881-884, 2008.

]. Pin98 and . Pin, Tropical semirings, Plo81] G. D. Plotkin. A structural approach to operational semantics, pp.50-69, 1981.
DOI : 10.1017/CBO9780511662508.004

D. Pretolani, A directed hypergraph model for random time dependent shortest paths, European Journal of Operational Research, vol.123, issue.2, pp.315-324, 2000.
DOI : 10.1016/S0377-2217(99)00259-3

D. Pretolani, Hypergraph Reductions and Satisfiability Problems, Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003, pp.383-397, 2003.
DOI : 10.1007/978-3-540-24605-3_29

B. [. Richter-gebert, T. Sturmfels, and . Theobald, First steps in tropical geometry, Idempotent mathematics and mathematical physics, pp.289-317, 2005.
DOI : 10.1090/conm/377/06998

]. H. Ric56 and . Gordon-rice, On completely recursively enumerable classes and their key arrays, J. Symb. Log, vol.21, issue.3, pp.304-308, 1956.

R. J. Pehrson, Software development for the Boeing 777, 1996.

X. Rival and L. Mauborgne, The trace partitioning abstract domain, ACM Transactions on Programming Languages and Systems, vol.29, issue.5, 2007.
DOI : 10.1145/1275497.1275501

[. Sans, Top 25 most dangerous programming errors, 2007.

R. Seidel, A convex hull algorithm optimal for point sets in even dimensions, 1981.

]. I. Sin97 and . Singer, Abstract convex analysis, 1997.

A. [. Simon and . King, Analyzing String Buffers in C, Algebraic Methodology and Software Technology, pp.365-379, 2002.
DOI : 10.1007/3-540-45719-4_25

. A. Skh03, A. Simon, J. M. King, and . Howe, Two Variables per Linear Inequality as an Abstract Domain Logic-Based Program Synthesis and Transformation, LNCS, vol.2664, pp.71-89, 2003.

[. Sagiv, T. Reps, and R. Wilhelm, Solving shape-analysis problems in languages with destructive updating, ACM Transactions on Programming Languages and Systems, vol.20, issue.1, pp.1-50, 1998.
DOI : 10.1145/271510.271517

T. W. Sagiv, R. Reps, and . Wilhelm, Parametric shape analysis via 3?valued logic, Symposium on Principles of Programming Languages, pp.105-118, 1999.
DOI : 10.1145/514188.514190
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.3161

H. [. Sankaranarayanan, Z. Sipma, and . Manna, Scalable Analysis of Linear Systems Using Mathematical Programming, Proceedings of VMCAI, volume 3385, 2005.
DOI : 10.1007/978-3-540-30579-8_2

B. Steensgaard, Points-to analysis in almost linear time, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '96, pp.32-41, 1996.
DOI : 10.1145/237721.237727

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

R. Tarjan, Depth-First Search and Linear Graph Algorithms, SIAM Journal on Computing, vol.1, issue.2, pp.146-160, 1972.
DOI : 10.1137/0201010

J. D. Ullman, Principle of database systems, Computer Science Press, 1982.

A. Venet and G. Brat, Precise and efficient static array bound checking for large embedded C programs, PLDI '04: Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, pp.231-242, 2004.

A. Venet, Nonuniform Alias Analysis of Recursive Data Structures and Arrays, SAS '02: Proceedings of the 9th International Symposium on Static Analysis, pp.36-51, 2002.
DOI : 10.1007/3-540-45789-5_6

A. Venet, A Scalable Nonuniform Pointer Analysis for Embedded Programs, Static Analysis, 11th International Symposium, SAS 2004, pp.149-164, 2004.
DOI : 10.1007/978-3-540-27864-1_13

]. N. Vor67 and . Vorobyev, Extremal algebra of positive matrices, Elektron. Informationsverarbeitung und Kybernetik, vol.3, pp.39-71, 1967.

M. Gunter and . Ziegler, Lectures on Polytopes, 1998.

M. Gunter and . Ziegler, Lectures on 0/1-polytopes, Polytopes ? combinatorics and computation (Oberwolfach, pp.1-41, 1997.

]. K. Zim77 and . Zimmermann, A general separation theorem in extremal algebras, Ekonom.- Mat. Obzor, vol.13, issue.2, pp.179-201, 1977.