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

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

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

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

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

C. Urban, The Abstract Domain of Segmented Ranking Functions, pp.43-62, 2013.
DOI : 10.1007/978-3-642-38856-9_5

URL : https://hal.archives-ouvertes.fr/hal-00925670

C. Urban and A. Miné, An Abstract Domain to Infer Ordinal-Valued Ranking Functions, 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, 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, pp.190-208, 2015.
DOI : 10.1007/978-3-662-46081-8_11

URL : https://hal.archives-ouvertes.fr/hal-01105238

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.77-102, 1997.
DOI : 10.1016/S0304-3975(00)00313-3

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

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

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

D. Park, Fixpoint Induction and Proofs of Program Properties, Machine Intelligence, vol.5, pp.59-78, 1969.

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

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

A. Miné, The octagon abstract domain, Higher-Order and Symbolic Computation, vol.2477, issue.3, pp.31-100, 2006.
DOI : 10.1007/s10990-006-8609-1

A. Chakarov and S. Sankaranarayanan, Expectation Invariants for Probabilistic Program Loops as Fixed Points, pp.85-100, 2014.
DOI : 10.1007/978-3-319-10936-7_6

A. Miné, Inferring Sufficient Conditions with Backward Polyhedral Under-Approximations, Electronic Notes in Theoretical Computer Science, vol.287, pp.89-100, 2012.
DOI : 10.1016/j.entcs.2012.09.009

B. Jeannet and A. Miné, Apron: A Library of Numerical Abstract Domains for Static Analysis, pp.661-667, 2009.
DOI : 10.1007/978-3-642-02658-4_52

URL : https://hal.archives-ouvertes.fr/hal-00786354

F. Bourdoncle, Efficient chaotic iteration strategies with widenings, pp.128-141, 1993.
DOI : 10.1007/BFb0039704

V. D. Silva and C. Urban, Conflict-Driven Conditional Termination, CAV (II), pp.271-286, 2015.

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

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

A. Podelski and A. Rybalchenko, Transition Predicate Abstraction and Fair Termination, pp.132-144, 2005.
DOI : 10.1145/1232420.1232422

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.592.2631

M. Y. Vardi, Verification of concurrent programs: the automata-theoretic framework*, Annals of Pure and Applied Logic, vol.51, issue.1-2, pp.79-98, 1991.
DOI : 10.1016/0168-0072(91)90066-U

C. S. Lee, N. D. Jones, and A. M. Ben-amram, The Size-Change Principle for Program Termination, pp.81-92, 2001.

D. Massé, Property Checking Driven Abstract Interpretation-Based Static Analysis, pp.56-69, 2003.
DOI : 10.1007/3-540-36384-X_8

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

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

E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. 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

B. Cook, H. Khlaaf, and N. Piterman, Faster temporal reasoning for infinite-state programs, 2014 Formal Methods in Computer-Aided Design (FMCAD), pp.75-82, 2014.
DOI : 10.1109/FMCAD.2014.6987598

B. Cook, H. Khlaaf, and N. Piterman, On Automation of CTL* Verification for Infinite-State Systems, CAV (I), pp.13-29, 2015.
DOI : 10.1007/978-3-319-21690-4_2

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

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