C. Alias, A. Darte, P. Feautrier, and L. Gonnord, Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs, SAS, pp.117-133, 2010.
DOI : 10.1007/978-3-642-15769-1_8
URL : https://hal.archives-ouvertes.fr/inria-00523298

J. Bertrane, P. Cousot, R. Cousot, J. Feret, L. Mauborgne et al., Static Analysis and Verification of Aerospace Software by Abstract Interpretation, AIAA, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00528611

A. R. Bradley, Z. Manna, and H. B. Sipma, Linear Ranking with Reachability, CAV, pp.491-504, 2005.
DOI : 10.1007/11513988_48

M. Brockschmidt, B. Cook, and C. Fuhs, Better Termination Proving through Cooperation, CAV, pp.413-429, 2013.
DOI : 10.1007/978-3-642-39799-8_28

H. Y. Chen, S. Flur, and S. Mukhopadhyay, Termination Proofs for Linear Simple Loops, SAS, pp.422-438, 2012.

M. Colón and H. Sipma, Practical Methods for Proving Program Termination, CAV, pp.442-454, 2002.
DOI : 10.1007/3-540-45657-0_36

B. Cook, S. Gulwani, T. Lev-ami, A. Rybalchenko, and M. Sagiv, Proving Conditional Termination, CAV, pp.328-340, 2008.
DOI : 10.1007/978-3-540-70545-1_32
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.125.9460

B. Cook, A. See, and F. Zuleger, Ramsey vs. Lexicographic Termination Proving, TACAS, pp.47-61, 2013.
DOI : 10.1007/978-3-642-36742-7_4

P. Cousot and R. Cousot, Static Determination of Dynamic Properties of Programs, Symposium on Programming, pp.106-130, 1976.

P. Cousot and R. Cousot, Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages), Proceedings of 1994 IEEE International Conference on Computer Languages (ICCL'94), pp.95-112, 1994.
DOI : 10.1109/ICCL.1994.288389

P. Cousot and R. Cousot, An Abstract Interpretation Framework for Termination, POPL, pp.245-258, 2012.

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

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-96, 1978.
DOI : 10.1145/512760.512770

R. W. Floyd, Assigning Meanings to Programs, Proceedings of Symposium on Applied Mathematics, pp.19-32, 1967.

H. Fuchs, Z. M. Kedem, and B. F. Naylor, On visible surface generation by a priori tree structures, ACM SIGGRAPH Computer Graphics, vol.14, issue.3, pp.124-133, 1980.
DOI : 10.1145/965105.807481

P. Ganty and S. Genaim, Proving Termination Starting from the End, CAV, pp.397-412, 2013.
DOI : 10.1007/978-3-642-39799-8_27

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

J. Giesl, P. Schneider-kamp, and R. Thiemann, Automatic Termination Proofs in the Dependency Pair Framework, IJCAR, pp.281-286, 2006.

A. Gurfinkel and S. Chaki, Boxes: A Symbolic Abstract Domain of Boxes, SAS, pp.287-303, 2010.
DOI : 10.1007/978-3-642-15769-1_18

A. Gurfinkel and S. Chaki, Combining predicate and numeric abstraction for software model checking, International Journal on Software Tools for Technology Transfer, vol.2, issue.4, pp.409-427, 2010.
DOI : 10.1007/s10009-010-0162-x

M. Heizmann, J. Hoenicke, J. Leike, and A. Podelski, Linear Ranking for Linear Lasso Programs, ATVA, pp.365-380, 2013.
DOI : 10.1007/978-3-319-02444-8_26

B. Jeannet, Representing and Approximating Transfer Functions in Abstract Interpretation of Hetereogeneous Datatypes, SAS, pp.52-68, 2002.
DOI : 10.1007/3-540-45789-5_7