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

T. A. Beyene, C. Popeea, and A. Rybalchenko, Solving Existentially Quantified Horn Clauses, CAV, pp.869-882, 2013.
DOI : 10.1007/978-3-642-39799-8_61

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, FMCAD, pp.144-153, 2011.

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

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

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

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

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

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

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

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

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

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

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

A. Miné, Inferring Sufficient Conditions with Backward Polyhedral Under-Approximations, NSAD, pp.89-100, 2012.
DOI : 10.1016/j.entcs.2012.09.009

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.
DOI : 10.1145/1232420.1232422

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

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

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, 2014.
DOI : 10.1007/978-3-319-10936-7_19

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

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