A. , 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.
URL : https://hal.archives-ouvertes.fr/inria-00523298

M. Amir, C. S. Ben-amram, and . Lee, Ranking Functions for Size-Change Termination II, Logical Methods in Computer Science, vol.5, issue.2, 2009.

[. Biere, C. Artho, and V. Schuppan, Liveness Checking as Safety Checking, Electronic Notes in Theoretical Computer Science, vol.66, issue.2, pp.160-177, 2002.
DOI : 10.1016/S1571-0661(04)80410-9

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

P. Bcc-+-10-]-julien-bertrane, R. Cousot, J. Cousot, L. Feret, and . Mauborgne, Antoine Miné, and Xavier Rival. Static Analysis and Verification of Aerospace Software by Abstract Interpretation, AIAA, 2010.

[. Berdine, B. Cook, D. Distefano, and P. W. Hearn, Automatic Termination Proofs for Programs with Shape-Shifting Heaps, CAV, pp.386-400, 2006.
DOI : 10.1007/11817963_35

[. 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
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.296.8328

[. 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 : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.7610

R. Bms05a-]-aaron, Z. Bradley, H. B. Manna, and . Sipma, Linear Ranking with Reachability, CAV, pp.491-504, 2005.

R. Bms05b-]-aaron, Z. Bradley, H. B. Manna, and . Sipma, The Polyranking Principle, ICALP, pp.1349-1361, 2005.

[. Bourdoncle, Ecient Chaotic Iteration Strategies with Widenings, FMPA, pp.128-141, 1993.

A. Tewodros, C. Beyene, A. Popeea, and . Rybalchenko, Solving Existentially Quantified Horn Clauses, CAV, pp.869-882, 2013.

A. R. Bradley, SAT-Based Model Checking without Unrolling, VMCAI, pp.70-87, 2011.
DOI : 10.1007/3-540-40922-X_8

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

R. Aaron, F. Bradley, Z. Somenzi, Y. Hassan, and . Zhang, An Incremental Approach to Model Checking Progress Properties, FMCAD, pp.144-153, 2011.

G. Cantor, Beitr??ge zur Begr??ndung der transfiniten Mengenlehre, Mathematische Annalen, vol.46, issue.4, pp.481-512
DOI : 10.1007/BF02124929

G. Cantor, Beitr???ge zur Begr???ndung der transfiniten Mengenlehre, Mathematische Annalen, vol.49, issue.2, pp.207-246, 1897.
DOI : 10.1007/BF01444205

P. Cousot and R. Cousot, Static Determination of Dynamic Properties of Programs, Symposium 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, 1977.
DOI : 10.1145/512950.512973
URL : https://hal.archives-ouvertes.fr/hal-01108790

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, Abstract interpretation and application to logic programs, The Journal of Logic Programming, vol.13, issue.2-3, pp.103-179, 1992.
DOI : 10.1016/0743-1066(92)90030-7

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, Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, PLILP, pp.269-295, 1992.
DOI : 10.1007/3-540-55844-6_142

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 for Peace and Security Series -D: Information and Communication Security, pp.1-29, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00543886

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

[. 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

E. M. Clarke and E. Emerson, Design and Synthesis of Synchronization Skeletons using Branching-Time Temporal Logic, Workshop on Logics of Programs, pp.52-71, 1981.

O. Clarke, S. Grumberg, Y. Jha, H. Lu, and . Veith, Counterexample-guided abstraction refinement for symbolic model checking, Journal of the ACM, vol.50, issue.5, pp.752-794, 2003.
DOI : 10.1145/876638.876643

S. Cook, T. Gulwani, A. Lev-ami, M. Rybalchenko, and . 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

A. Cook, A. Gotsman, A. Podelski, M. Y. Rybalchenko, and . Vardi, Proving that Programs Eventually do Something Good, POPL, pp.265-276, 2007.

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

[. Cook and E. Koskinen, Reasoning About Nondeterminism in Programs, PLDI, pp.219-230, 2013.

[. Cousot, Méthodes Itératives de Construction et d'Appro ximation de Points Fixes d'Opérateurs Monotones sur un Treil lis, Analyse Sémantique de Programmes, Thèse d' ´ Etat`EsEtat` Etat`Es Scien ces MathématiquesCou97] Patrick Cousot. Constructive Design of a Hierarchy of Semantics of a Transition System by Abstract Interpretation. Electronic Notes in Theoretical Computer Science, pp.77-102, 1978.

[. 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

[. Cousot, Abstracting Induction by Extrapolation and Interpolation, VMCAI, pp.19-42, 2015.
DOI : 10.1007/978-3-662-46081-8_2

[. Cook, A. Podelski, and A. Rybalchenko, Terminator: Beyond Safety, CAV, pp.415-418, 2006.
DOI : 10.1007/11817963_37

[. Cook, A. Podelski, and A. Rybalchenko, Proving program termination, Communications of the ACM, vol.54, issue.5, pp.88-98, 2011.
DOI : 10.1145/1941487.1941509

[. Chang and X. Rival, Modular Construction of Shape-Numeric Analyzers, Festschrift for Dave Schmidt, pp.161-185, 2013.
DOI : 10.4204/EPTCS.129.11
URL : https://hal.archives-ouvertes.fr/hal-00926948

M. Colón and H. Sipma, Synthesis of Linear Ranking Functions, TACAS, pp.67-81, 2001.
DOI : 10.1007/3-540-45319-9_6

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

[. Cook, A. See, F. Zuleger, K. Ramsey-vs-saumya, N. Debray et al., Lexicographic Termination Proving Task Granularity Analysis in Logic Programs, TACAS PLDI, pp.47-61, 1990.

D. Vijay, C. Silva, and . Urban, Conflict-Driven Abstract Interpretation for Conditional Termination, CAV, 2015.

J. Feret, The Arithmetic-Geometric Progression Abstract Domain, VMCAI, pp.42-58, 2005.
DOI : 10.1007/978-3-540-30579-8_3
URL : https://hal.archives-ouvertes.fr/inria-00528450

[. 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

R. W. Floyd, Assigning meanings to programs, Proceedings of Symposium on Applied Mathematics, vol.19, pp.19-32, 1967.
DOI : 10.1090/psapm/019/0235771

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

[. Gotsman, B. Cook, M. J. Parkinson, and V. Vafeiadis, Proving that Non-Blocking Algorithms Don't Block, POPL, pp.16-28, 2009.

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

L. Gonnord, D. Monniaux, and G. Radanne, Synthesis of Ranking Functions using Extremal Counterexamples, PLDI, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01144622

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

P. Granger, Static Analysis of Arithmetic Congruences, International Journal of Computer Math, pp.165-199, 1989.

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

M. Heizmann, D. Dietsch-leike, B. Musa, and A. Podelski, Ultimate Automizer with Array Interpolation (Competition Contribution), TACAS, 2015.

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

[. Heizmann, N. D. Jones, and A. Podelski, Size-Change Termination and Transition Invariants, SAS, pp.22-50, 2010.
DOI : 10.1007/978-3-642-15769-1_4
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.167.8500

[. Hoare, An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-580, 1969.
DOI : 10.1145/363235.363259

[. 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

[. Jeannet and A. Miné, Apron: A Library of Numerical Abstract Domains for Static Analysis, CAV, pp.661-667, 2009.
DOI : 10.1007/978-3-642-02658-4_52
URL : https://hal.archives-ouvertes.fr/hal-00786354

[. Kaser, C. R. Ramakrishnan, and S. Pawagi, On the conversion of indirect to direct recursion, ACM Letters on Programming Languages and Systems, vol.2, issue.1-4, pp.151-164, 1993.
DOI : 10.1145/176454.176510

[. Kunen, Set Theory: An Introduction to Independence Proofs, Studies in Logic and the Foundations of Mathematics, 1980.

L. Lamport, Proving the Correctness of Multiprocess Programs, IEEE Transactions on Software Engineering, vol.3, issue.2, pp.125-143, 1977.
DOI : 10.1109/TSE.1977.229904

[. Lee, Ranking functions for size-change termination, ACM Transactions on Programming Languages and Systems, vol.31, issue.3, p.31, 2009.
DOI : 10.1145/1498926.1498928

[. Lee, N. D. Jones, M. Amir, and . Ben-amram, The Size-Change Principle for Program Termination, POPL, pp.81-92, 2001.

[. Larsen, F. Larsson, P. Pettersson, and W. Yi, Ecient Verification of Real-Time Systems: Compact Data Structure and State-Space Reduction, RTSS, pp.14-24, 1997.

[. Larraz and A. Oliveras, Enric Rodríguez-Carbonell, and Albert Rubio. Proving Termination of Imperative Programs using Max-SMT, FMCAD, pp.218-225, 2013.

[. Le, S. Qin, and W. Chin, Termination and Non-Termination Specification Inference Property Checking Driven Abstract Interpretation-Based Static Analysis, PLDI, 2015. [Mas03] Damien Massé VMCAI, pp.56-69, 2003.

D. Massé, Abstract Domains for Property Checking Driven Analysis of Temporal Properties, AMAST, pp.349-363, 2004.
DOI : 10.1007/978-3-540-27815-3_28

D. Massé, Policy Iteration-Based Conditional Termination and Ranking Functions, VMCAI, pp.453-471, 2014.
DOI : 10.1007/978-3-642-54013-4_25

[. Muthukumar and M. V. Hermenegildo, Compile-time derivation of variable dependency using abstract interpretation, The Journal of Logic Programming, vol.13, issue.2-3, pp.315-347, 1992.
DOI : 10.1016/0743-1066(92)90035-2

A. Miné, Weakly Relational Numerical Abstract Domains, 2004.

A. Miné, The Octagon Abstract Domain. Higher-Order and Symbolic Computation, pp.31-100, 2006.

A. Miné, Relational Thread-Modular Static Value Analysis by Abstract Interpretation, VMCAI, pp.39-58, 2014.
DOI : 10.1007/978-3-642-54013-4_3

[. Morris and C. B. Jones, An Early Program Proof by Alan Turing, IEEE Annals of the History of Computing, vol.6, issue.2, pp.139-143, 1984.
DOI : 10.1109/MAHC.1984.10017

B. Jesper, J. Møller, H. R. Lichtenberg, H. Andersen, and . Hulgaard, Di?erence decision diagrams, CSL, pp.111-125, 1999.

R. E. Moore, Interval Analysis, 1966.

[. Manna and A. Pnueli, A hierarchy of temporal properties, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing , PODC '87, pp.377-410, 1990.
DOI : 10.1145/41840.41857

[. Manna and A. Pnueli, The Temporal Verification of Reactive Systems: Progress, 1996.
DOI : 10.1007/978-1-4612-4222-2

[. Owre, J. M. Rushby, and N. Shankar, PVS: A prototype verification system, CADEPar69] David Park. Fixpoint Induction and Proofs of Program Properties . Machine Intelligence, pp.748-75259, 1969.
DOI : 10.1007/3-540-55602-8_217

L. Gary and . Peterson, Myths About the Mutual Exclusion Problem, Information Processing Letters, vol.12, issue.3, pp.115-116, 1981.

A. Podelski and A. Rybalchenko, A Complete Method for the Synthesis of Linear Ranking Functions, VMCAI, pp.239-251, 2004.
DOI : 10.1007/978-3-540-24622-0_20

A. Podelski and A. Rybalchenko, Transition invariants, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004., pp.32-41, 2004.
DOI : 10.1109/LICS.2004.1319598

A. Podelski and A. Rybalchenko, Transition Predicate Abstraction and Fair Termination, POPL, pp.132-144, 2005.

J. Queille and J. Sifakis, Specification and verification of concurrent systems in CESAR, 5th International Symposium on Programming, pp.337-351, 1982.
DOI : 10.1007/3-540-11494-7_22

T. Ströder, C. Aschermann, F. Frohn, J. Hensel, and J. Giesl, AProVE: Termination and Memory Safety of C Programs (Competition Contribution), TACAS, 2015.

[. Sankaranarayanan, F. Ivancic, I. Shlyakhter, and A. Gupta, Static Analysis in Disjunctive Numerical Domains, SAS, pp.3-17, 2006.
DOI : 10.1007/11823230_2

[. Serrano, P. López-garcía, and M. V. Hermenegildo, Abstract, Theory and Practice of Logic Programming, vol.34, issue.4-5, pp.4-5739, 2014.
DOI : 10.1016/0743-1066(92)90035-2
URL : https://hal.archives-ouvertes.fr/hal-01185400

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

[. Tsitovich, N. Sharygina, C. M. Wintersteiger, and D. Kroening, Loop Summarization and Termination Analysis, TACAS, pp.81-95, 2011.
DOI : 10.1007/11609773_18

A. Turing, On Computable Numbers, with An Application to the Entscheidungs Problem, pp.230-265, 1936.

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é, An Abstract Domain to Infer Ordinal-Valued Ranking Functions, ESOP, pp.412-431, 2014.
DOI : 10.1007/978-3-642-54833-8_22
URL : https://hal.archives-ouvertes.fr/hal-00925731

C. Urban and A. Miné, A Decision Tree Abstract Domain for Proving Conditional Termination, SAS, pp.302-318, 2014.
DOI : 10.1007/978-3-319-10936-7_19
URL : https://hal.archives-ouvertes.fr/hal-01105221

C. Urban and A. Miné, Proving Guarantee and Recurrence Temporal Properties by Abstract Interpretation, VM- CAI, 2015.
DOI : 10.1007/978-3-662-46081-8_11
URL : https://hal.archives-ouvertes.fr/hal-01105238

[. Urban, The Abstract Domain of Segmented Ranking Functions, SAS, pp.43-62, 2013.
DOI : 10.1007/978-3-642-38856-9_5
URL : https://hal.archives-ouvertes.fr/hal-00925670

[. Urban, Piecewise-Defined Ranking Functions, WST, pp.69-73, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00925682

[. Urban, FuncTion: An Abstract Domain Functor for Termination (Competition Contribution), TACAS, 2015.

M. Y. Vardi, Verification of Concurrent Programs: The Automata-Theoretic Framework. Annals of Pure and Applied Logic, pp.79-98, 1991.

A. Scientiarum and M. , [Weg75] Ben Wegbreit. Mechanical Program Analysis, Communications of the ACM, vol.1, issue.189, pp.199-208528, 1923.