A. V. Aho, R. Sethi, and J. D. Ullman, Compilers, Principles Techniques and Tools, 1986.

E. Albert, P. Arenas, C. Codish, S. Genaim, G. Puebla et al., Termination analysis of Java bytecode, Proc. of Formal Methods for Open Object-Based Distributed Systems, 10th IFIP WG 6.1 International Conference, FMOODS'08, vol.5051, pp.2-18, 2008.
DOI : 10.1007/978-3-540-68863-1_2
URL : https://link.springer.com/content/pdf/10.1007%2F978-3-540-68863-1_2.pdf

T. Armstrong, K. Marriott, P. Schachte, and H. Søndergaard, Two classes of Boolean functions for dependency analysis, Sci. Comput. Program, vol.31, issue.1, pp.3-45, 1998.

R. Bagnara, P. M. Hill, and E. Zaffanella, The Parma polyhedra library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems, Sci. Comput. Program, vol.72, issue.1-2, pp.3-21, 2008.

F. Bancilhon, D. Maier, Y. Sagiv, and J. Ullman, Magic sets and other strange ways to implement logic programs, Proc. of the 5th ACM Symposium on Principles of Database Systems, pp.1-15, 1986.
DOI : 10.1145/6012.15399

M. Barnett, B. E. Chang, R. Deline, B. Jacobs, K. R. Boogie et al., 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.
DOI : 10.1007/11804192_17
URL : https://www.microsoft.com/en-us/research/wp-content/uploads/2005/01/krml160.pdf

M. Barnett, M. Fahndrich, and F. Logozzo, Foxtrot and Clousot: Language agnostic dynamic and static contract checking for .NET, 2008.

C. Beeri and R. Ramakrishnan, On the power of magic, J. Log. Program, vol.10, issue.3 & 4, pp.255-300, 1991.

C. Bodei, P. Degano, F. Nielson, and H. R. Nielson, Static analysis for secrecy and non-interference in networks of processes, Proc. of PaCT'01, vol.2127, pp.27-41, 2001.

R. E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Trans. Comput, vol.35, issue.8, pp.677-691, 1986.
DOI : 10.1109/tc.1986.1676819
URL : http://www.cs.cmu.edu/~bryant/pubs.pdf

D. Clark, C. Hankin, and S. Hunt, Information flow for ALGOL-like languages, Comput. Lang, vol.28, issue.1, pp.3-28, 2002.
DOI : 10.1016/s0096-0551(02)00006-1

M. Codish, Efficient goal directed bottom-up evaluation of logic programs, J. Log. Program, vol.38, issue.3, pp.355-370, 1999.
DOI : 10.1016/s0743-1066(98)10024-9
URL : https://doi.org/10.1016/s0743-1066(98)10024-9

M. Codish, D. Dams, and E. Yardeni, Bottom-up abstract interpretation of logic programs, J. Theor. Comput. Sci, vol.124, pp.93-125, 1994.
DOI : 10.1016/0304-3975(94)90055-8
URL : https://doi.org/10.1016/0304-3975(94)90055-8

B. Cook, A. Podelski, and A. Rybalchenko, Termination proofs for systems code, Proc. of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation (PLDI'06), pp.415-426, 2006.
DOI : 10.1145/1133981.1134029
URL : http://www.sct.inf.ethz.ch/teaching/ws2006/SemSpecVer/papers/cook_termination_proofs.pdf

P. Cousot and R. Cousot, 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.

P. Cousot and R. Cousot, Systematic design of program analysis frameworks, Proc. of the 6th ACM Symposium on Principles of Programming Languages (POPL'79), pp.269-282, 1979.
DOI : 10.1145/567752.567778
URL : http://www.di.ens.fr/~rcousot/publi/POPL79.pdf

P. Cousot and R. Cousot, Abstract interpretation and applications to logic programs, J. Log. Program, vol.13, issue.2 & 3, pp.103-179, 1992.
DOI : 10.1016/0743-1066(92)90030-7
URL : https://doi.org/10.1016/0743-1066(92)90030-7

P. Cousot and N. Halbwachs, Automatic discovery of linear restraints among variables of a program, Proc. Fifth ACM Symp. Principles of Programming Languages, pp.84-96, 1978.

O. Danvy and A. Filinski, Representing control, a study of the CPS transformation, Math. Struct. Comput. Sci, vol.2, issue.4, pp.361-391, 1992.

L. Hubert, T. Jensen, and D. Pichardie, Semantic foundations and inference of non-null annotations, Proc. of the 10th International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS'08), pp.142-149, 2008.
DOI : 10.1007/978-3-540-68863-1_9
URL : https://hal.archives-ouvertes.fr/inria-00266171

G. Klein and T. Nipkow, A machine-checked model for a Java-like language, virtual machine, and compiler, ACM Trans. Program. Lang. Syst. (TOPLAS), vol.28, issue.4, pp.619-695, 2006.
DOI : 10.1145/1146809.1146811
URL : http://dl.acm.org/ft_gateway.cfm?id=1146811&type=pdf

P. Laud, Semantics and program analysis of computationally secure information flow, Proc. of the 10th European Symposium On Programming (ESOP'01), vol.2028, pp.77-91, 2001.
DOI : 10.1007/3-540-45309-1_6
URL : https://link.springer.com/content/pdf/10.1007%2F3-540-45309-1_6.pdf

K. R. Leino and P. Müller, Object invariants in dynamic contexts, Proc. of the 18th European Conference on Object-Oriented Programming (ECOOP'04), vol.3086, pp.491-516, 2004.
DOI : 10.1007/978-3-540-24851-4_22
URL : http://pag.csail.mit.edu/reading-group/leino04invariants.pdf

K. R. Leino and A. Wallenburg, Class-local object invariants, Proc. of the 1st India Software Engineering Conference (ISEC'08), pp.57-66, 2008.
DOI : 10.1145/1342211.1342225

T. Lindholm and F. Yellin, The Java TM Virtual Machine Specification, 1999.

F. Logozzo, Cibai: An abstract interpretation-based static analyzer for modular analysis and verification of Java classes, 8th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'07), vol.4349, pp.293-298, 2007.
DOI : 10.1007/978-3-540-69738-1_21

F. Logozzo, Class invariants as abstract interpretation of trace semantics, Comput. Lang. Syst. Struct, vol.35, issue.2, pp.100-142, 2009.
DOI : 10.1016/j.cl.2005.01.001

F. Logozzo and M. Fähndrich, On the relative completeness of bytecode analysis versus source code analysis, Proc. of the 17th International Conference on Compiler Construction, (CC'08), vol.4959, pp.197-212, 2008.
DOI : 10.1007/978-3-540-78791-4_14
URL : https://link.springer.com/content/pdf/10.1007%2F978-3-540-78791-4_14.pdf

M. Méndez, J. Navas, and M. V. Hermenegildo, An efficient, parametric fixpoint algorithm for incremental analysis of Java bytecode, Proc. of the Second Workshop on Bytecode Semantics, Verification, Analysis and Transformation, vol.190, pp.51-66, 2007.

A. Miné, A new numerical abstract domain based on difference-bound matrices, Proc. of the 2nd Symposium on Programs as Data Objects (PADO II), vol.2053, pp.155-172, 2001.

P. Müller, Reasoning about object structures using ownership, Proc. of the Workshop on Verified Software: Theories, Tools, Experiments (VSTTE'07), vol.4171, 2007.

J. Palsberg and M. I. Schwartzbach, Object-oriented type inference, Proc. of OOPSLA'91, vol.26, pp.146-161, 1991.

É. Payet and F. Spoto, Magic-sets transformation for the analysis of Java bytecode, Proceedings of the 14th International Static Analysis Symposium (SAS'07), vol.4634, pp.452-467, 2007.
URL : https://hal.archives-ouvertes.fr/hal-01916204

I. Pollet, B. Le-charlier, and A. Cortesi, Distinctness and sharing domains for static analysis of Java programs, 15th European Conference on Object-Oriented Programming (ECOOP'01), vol.2072, pp.77-98, 2001.

S. Rossignoli and F. Spoto, Detecting non-cyclicity by abstract compilation into boolean functions, Proc. of Verification, Model Checking and Abstract Interpretation, vol.3855, pp.95-110, 2006.

A. Sabelfeld and A. C. Myers, Language-based information-flow security, IEEE J. Sel. Areas Commun, vol.21, issue.1, pp.5-19, 2003.

D. A. Schmidt, Trace-based abstract interpretation of operational semantics, J. Lisp Symb. Comput, vol.10, issue.3, pp.237-271, 1998.

S. Secci and F. Spoto, Pair-sharing analysis of object-oriented programs, Proc. of the 12th Static Analysis Symposium (SAS'05), vol.3672, pp.320-335, 2005.

F. Spoto, Precise null-pointer analysis, J. Softw. Syst. Model

F. Spoto, Watchpoint semantics: a tool for compositional and focussed static analyses, Proceedings of the 8th International Static Analysis Symposium (SAS'01), vol.2126, pp.127-145, 2001.

F. Spoto, Nullness analysis in Boolean form, Proc. of the 6th IEEE International Conference on Software Engineering and Formal Methods (SEFM'08), pp.21-30, 2008.

F. Spoto, P. M. Hill, and É. Payet, Path-length analysis for object-oriented programs, Proc. of Emerging Applications of Abstract Interpretation, 2006.
URL : https://hal.archives-ouvertes.fr/hal-01915777

F. Spoto, F. Mesnard, and É. Payet, A termination analyzer for Java bytecode based on path-length, ACM Trans. Program. Lang. Syst, vol.32, issue.3, 2010.
URL : https://hal.archives-ouvertes.fr/hal-01186167

G. J. Sussman and G. L. Steele, Scheme: An interpreter for extended lambda calculus, AI Memo, vol.349, 1975.

G. J. Sussman and G. L. Steele, Scheme: An interpreter for extended lambda calculus. High.-Order Symb, Comput, vol.11, issue.4, pp.405-439, 1998.

A. Tarski, A lattice-theoretical fixpoint theorem and its applications, Pac. J. Math, vol.5, pp.285-309, 1955.

J. The and . Analyser,

D. Volpano, G. Smith, and C. Irvine, A sound type system for secure flow analysis, J. Comput. Secur, vol.4, issue.2, pp.167-187, 1996.

G. Winskel, The Formal Semantics of Programming Languages, 1993.