A. , A. V. Sethi, R. And, U. , and J. D. , Compilers, Principles Techniques and Tools, 1986.

A. , W. Baar, T. Beckert, B. Bubel, R. Giese et al., The KeY Tool. Software and System Modeling, vol.4, pp.32-54, 2005.

A. , E. Arenas, P. Codish, M. Genaim, S. Puebla et al., Termination Analysis of Java Bytecode, Proc. of the 9th International Workshop on Termination (WST'07), 2007.

A. , E. Arenas, P. Codish, M. Genaim, S. Puebla et al., Termination Analysis of Java Bytecode, Proc. of the International Conference on Formal Methods for Open ObjectBased Distributed Systems (FMOODS'08, vol.5051, pp.2-18, 2008.

A. , E. Arenas, P. Genaim, S. Puebla, G. And et al., Cost Analysis of Java Bytecode, Proc. of the 16th European Symposium on Programming, vol.4421, pp.157-172, 2007.

A. and J. , Size-change Termination and Bound Analysis, Proc. of the 8th International Symposium on Functional and Logic Programming (FLOPS'06, vol.3945, pp.192-207, 2006.

B. , D. Hu, A. J. Rakamaric, Z. And, C. et al., Proving Termination by Divergence, Proc. of the 5th IEEE International Conference on Software Engineering and Formal Methods (SEFM'07), pp.93-102, 2007.

D. F. Bacon and P. F. Sweeney, Fast Static Analysis of C++ Virtual Function Calls, Proc. of the Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA'96), vol.31, pp.324-341, 1996.

B. , R. Hill, P. M. Ricci, E. And, Z. et al., Precise Widening Operators for Convex Polyhedra, Science of Computer Programming, vol.58, pp.28-56, 2005.

B. , R. Hill, P. M. And, Z. , and E. , 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, pp.1-2, 2008.

B. , F. And-m-¨-uller, and P. , A Program Logic for Bytecode, Electronic Notes on Theoretical Computer Science, vol.141, pp.255-273, 2005.

B. , M. Chang, B. E. Deline, R. Jacobs, B. And et al., Boogie: A Modular Reusable Verifier for Object-Oriented Programs, Proc. of the 4th International Symposium on Formal Methods for Components and Objects (FMCO'05), vol.4111, pp.364-387, 2005.

B. , A. M. Lee, and C. S. , Program Termination Analysis in Polynomial Time, ACM Transactions on Programming Languages and Systems (TOPLAS), vol.29, p.1, 2007.

B. , J. Calcagno, C. Cook, B. Distefano, D. O'hearn et al., Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming, Proc. of the 6th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'05, vol.3385, pp.1-24, 2007.

C. , P. And-cousot, and R. , Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints, Proc. of the 4th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'77, pp.238-252, 1977.

C. , P. And-cousot, and R. , Systematic Design of Program Analysis Frameworks, Proc. of the 6th ACM Symposium on Principles of Programming Languages (POPL'79), pp.269-282, 1979.

C. , P. And, and N. Halbwachs, Automatic Discovery of Linear Restraints among Variables of a Program, Proc. of the 5th ACM Symposium on Principles of Programming Languages (POPL'78), pp.84-96, 1978.

D. De-schreye and S. And-decorte, Termination of Logic Programs: The Never-Ending Story, Journal of Logic Programming, vol.19, pp.199-260, 1994.

D. , J. Grove, D. And, C. , and C. , Optimization of Object-Oriented Programs using Static Class Hierarchy Analysis, Proc. of the 9th European Conference on Object-Oriented Programming, vol.952, pp.77-101, 1995.

D. , N. Lindenstrauss, N. Sagiv, Y. And, S. et al., A General Framework for Automatic Termination Analysis of Logic Programs. Applicable Algebra in Engineering, Communication and Computing, vol.12, issue.2, pp.117-156, 2001.

D. , D. O'hearn, P. W. And, Y. , and H. , A Local Shape Analysis Based on Separation Logic, Proc. of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'06, vol.3920, pp.287-302, 2006.

F. and R. W. , Assigning Meanings to Programs, Mathematical Aspects of Computer Science, vol.19, pp.19-32, 1967.

G. , M. And-giacobazzi, and R. , Goal Independency and Call Patterns in the Analysis of Logic Programs, Proc. of the ACM Symposium on Applied Computing (SAC'94), pp.394-399, 1994.

G. , S. And, C. , and M. , Inferring Termination Conditions for Logic Programs using Backwards Analysis, Theory and Practice of Logic Programming (TPLP), vol.5, pp.75-91, 2005.

G. , S. And, and F. Spoto, Proc. of the 10th Workshop on Formal Techniques for Java-like Programs (FTfJP'08), M. Huisman, 2008.

G. , J. Schneider-kamp, P. And, T. , and R. , Automatic Termination Proofs in the Dependency Pair Framework, 3th International Joint Conference on Automated Reasoning (IJCAR'06, vol.4130, pp.281-286, 2006.

G. , A. Berdine, J. And, C. , and B. , Interprocedural Shape Analysis with Separated Heap Abstractions, Proc. of the 13th International Static Analysis Symposium (SAS'06, vol.4134, pp.240-260, 2006.

I. , S. S. And-o'hearn, and P. W. , BI as an Assertion Language for Mutable Data Structures, Proc. of the 28th Symposium on Principles of Programming Languages (POPL'01), pp.14-26, 2001.

J. , J. And, and M. J. Maher, Constraint Logic Programming: A Survey, Journal of Logic Programming, vol.19, pp.503-581, 1994.

K. , G. And-nipkow, and T. , A Machine-Checked Model for a Java-Like Language, Virtual Machine, and Compiler, ACM Transactions on Programming Languages and Systems (TOPLAS), vol.28, pp.619-695, 2006.

L. , G. T. Leino, K. R. And-m-¨-uller, and P. , Specification and Verification Challenges for Sequential Object-Oriented Programs, Formal Aspects of Computing, vol.19, pp.159-189, 2007.

L. , C. S. Jones, N. D. , A. Ben-amram, and A. M. , The Size-Change Principle for Program Termination, Proc. of the 28th Symposium on Principles of Programming Languages (POPL'01), pp.81-92, 2001.

L. , H. And-m-¨-uller, and P. , Formal Translation of Bytecode into BoogiePL. Electric Notes on Theoretical Computer Science, vol.190, pp.35-50, 2007.

·. F. Spoto, F. Mesnard, E. Payet, L. , K. R. And-m-¨-uller et al., Modular Verification of Static Class Invariants, Proc. of the 18th European Conference on Object-Oriented Programming, vol.3086, pp.26-42, 2004.

L. , K. R. And-wallenburg, and A. , Class-local Object Invariants, Proc. of the 1st India Software Engineering Conference (ISEC'08), 2008.

L. , T. And-yellin, and F. , The Java TM Virtual Machine Specification, 1999.

L. , G. Mehlitz, P. C. And, V. , and W. , Model Checking Real Time Java using Java PathFinder, Proc. of the 3rd International Symposium on Automated Technology for Verification and Analysis, vol.3707, pp.444-456, 2005.

L. , A. Reps, T. W. And, S. , and M. , Refinement-Based Verification for Possibly-Cyclic Lists, Proc. of Theory and Practice of Program Analysis and Compilation, Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday, vol.4444, pp.247-272, 2006.

L. , F. And-f-¨-ahndrich, and M. , On the Relative Completeness of Bytecode Analysis versus Source Code Analysis, Proc. of the 17th International Conference on Compiler Construction (CC'08, pp.197-212, 2008.

M. , P. And, and D. Vroon, Integrating Static Analysis and General-Purpose Theorem Proving for Termination Analysis, Proc. of the 28th International Conference on Software Engineering (ICSE'06, pp.873-876, 2006.

M. , P. And, and D. Vroon, Termination Analysis with Calling Context Graphs, Proc. of the 18th International Conference on Computer Aided Verification (CAV'06, vol.4144, pp.401-414, 2006.

M. , J. And, and W. Pugh, Core Semantics of Multithreaded Java, Proc. of the ACM Java Grande Conference, pp.29-38, 2001.

M. , J. Pugh, W. And, A. , and S. V. , The Java Memory Model, Proc. of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'05, pp.378-391, 2005.

M. and F. , Inferring Left-terminating Classes of Queries for Constraint Logic Programs, Proceedings of the 1996 Joint Int. Conference and Symposium on Logic Programming, pp.7-21, 1996.

M. , F. And, and R. Bagnara, cTI: a constraint-based Termination Inference tool for ISO-Prolog, Theory and Practice of Logic Programming, vol.5, pp.243-257, 2005.

M. , F. And, and A. Serebrenik, Recurrence with Affine Level Mappings is P-time Decidable for CLP(R), Theory and Practice of Logic Programming, vol.8, pp.111-119, 2008.

M. and A. , The Octagon Abstract Domain. Higher-Order and Symbolic Computation 19, vol.1, pp.31-100, 2006.

M. , D. ;. , and P. , The Pitfalls of Verifying Floating-Point Computations, Proc. of the Workshop on Verified Software: Theories, Tools, Experiments (VSTTE'07, vol.30, 2007.

P. , J. And, and M. I. Schwartzbach, Object-Oriented Type Inference, Proc. of the Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA'91, vol.26, pp.146-161, 1991.

P. , E. And, and F. Spoto, Magic-Sets Transformation for the Analysis of Java Bytecode, Proc. of the 14th International Static Analysis Symposium (SAS'07), vol.4634, pp.452-467, 2007.

P. and N. , Pure Versus Impure Lisp, ACM Transactions on Programming Languages and Systems, vol.19, pp.223-238, 1997.

P. Pl¨umer and L. , Termination Proofs for Logic Programs, Lecture Notes in Computer Science, vol.446, 1990.

P. , A. And-rybalchenko, and A. , A Complete Method for Synthesis of Linear Ranking Functions, Proc. of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'04, vol.2937, pp.239-251, 2004.

P. , A. And-rybalchenko, and A. , Transition Invariants, Proc. of the 19th IEEE Symposium on Logic in Computer Science (LICS'04), pp.32-41, 2004.

P. , A. And-rybalchenko, and A. , Transition Predicate Abstraction and Fair Termination, ACM Transactions on Programming Languages and Systems (TOPLAS), vol.29, p.3, 2007.

P. , I. Le-charlier, B. And, C. , and A. , Distinctness and Sharing Domains for Static Analysis of Java Programs, Proc. of the 15th European Conference on Object-Oriented Programming (ECOOP'01), vol.2072, pp.77-98, 2001.

R. and J. C. , Intuitionistic Reasoning about Shared Mutable Data Structure, Proc. of Millennial Perspectives in Computer Science, Symposium in Honour of Sir Tony Hoare, pp.303-321, 2000.

R. , S. And, and F. Spoto, Detecting Non-Cyclicity by Abstract Compilation into Boolean Functions, Proc. of the 7th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'06, vol.3855, pp.95-110, 2006.

S. , A. And-rinard, and M. C. , Purity and Side Effect Analysis for Java Programs, Proc. of the 6th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'05, vol.3385, pp.199-215, 2005.

S. , P. Giesl, J. Serebrenik, A. And, T. et al., Automated Termination Analysis for Logic Programs by Term Rewriting, Proc. of the 16th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'06), vol.4407, pp.177-193, 2006.

S. , S. And, and F. Spoto, Pair-Sharing Analysis of Object-Oriented Programs, Proc. of Static Analysis Symposium (SAS'05, vol.3672, pp.320-335, 2005.

S. , A. And, and D. De-schreye, On Termination of Logic Programs with Floating Point Computations, Proc. of the 9th International Symposium on Static Analysis (SAS'02, vol.2477, pp.151-164, 2002.

S. and F. , The JULIA Static Analyser, 2008.

S. and F. , Nullness Analysis in Boolean Form, Proc. of the 6th IEEE International Conference on Software Engineering and Formal Methods (SEFM'08), 2008.

S. , F. Hill, P. M. And, P. , and E. , Path-Length Analysis for Object-Oriented Programs, First International Workshop on Emerging Applications of Abstract Interpretation (EAAI'06), 2006.
URL : https://hal.archives-ouvertes.fr/hal-01915777

S. , F. And, and T. Jensen, Class Analyses as Abstract Interpretations of Trace Semantics, ACM Transactions on Programming Languages and Systems (TOPLAS), vol.25, pp.578-630, 2003.

S. , F. Lu, L. And, M. , and F. , Using CLP Simplifications to Improve Java Bytecode Termination Analysis, 2008.
URL : https://hal.archives-ouvertes.fr/hal-01188704

S. , F. Mesnard, F. And, P. , and E. , Julia + BinTerm: An Automatic Termination Prover for Java Bytecode, 2008.

S. and B. , Points-to Analysis in Almost Linear Time, Proc. of the 23th ACM Symposium on Principles of Programming Languages (POPL'96), pp.32-41, 1996.

S. , J. And-witzgall, and C. , Convexity and Optimization in Finite Dimensions I, 1970.

S. , D. Berger, F. Schwoon, S. And, E. et al., jMoped: A Test Environment for Java Programs, Proc. of the 19th International Conference on Computer Aided Verification (CAV'07, vol.4590, pp.164-167, 2007.

S. , D. Schwoon, S. And, E. , and J. , jMoped: A Java Bytecode Checker Based on Moped, Proc. of the 11th International Conference on Tools and Algorithms for the Construction and, 2005.