M. Abadi and L. Cardelli, A Theory of Objects, 1996.
DOI : 10.1007/978-1-4419-8598-9

A. Aggarwal and K. H. Randall, Related field analysis, Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '01)) of SIGPLAN Notices, pp.214-220, 2001.
DOI : 10.1145/381694.378850

P. America, Inheritance and Subtyping in a Parallel Object-Oriented Language, Proceedings of the European Conference on Object-Oriented Programming, pp.234-242, 1987.
DOI : 10.1007/3-540-47891-4_22

A. Inc, The Objective-C programming language Available online at http://developer.apple.com/documentation

K. Arnout and B. Meyer, Finding Implicit Contracts in .NET Components, First International Symposium on Formal Methods for Components and Objects, pp.285-318, 2002.
DOI : 10.1007/978-3-540-39656-7_12

R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella, Precise widening operators for convex polyhedra, Proceedings of the 10th Static Analysis Symposium 2003 (SAS '03), volume 2694 of Lectures Notes in Computer Science, pp.337-354, 2003.

B. Blanchet, Escape analysis for object oriented languages Application to Java, 14th ACM SIGPLAN Conference on Object-Oriented Programming , Systems, Languages and Applications (OOPSLA'99), pp.20-34, 1999.

B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne et al., A static analyzer for large safety-critical software, Proceedings of the 2003 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'03), pp.196-207, 2003.
URL : https://hal.archives-ouvertes.fr/hal-00128135

E. Börger, The origins and the development of the ASM method for high level system design and analysis, Journal of Universal Computer Science, vol.8, 2002.

B. Inc, Turbo Pascal 5.5 Object Oriented Programming Guide Available on- line at http://community, Borland Inc, 1989.

G. Bracha and W. R. Cook, Mixin-based inheritance, Proceedings of the 5th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA '90) SIGPLAN Notices, pp.303-311, 1990.
DOI : 10.1145/97946.97982
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.156.4510

M. Campione, K. Walrath, and A. Huml, The Java Tutorial: A Short Course on the Basics, 2000.

G. Cantor, Contributions to the founding of the theory of transfinite numbers (1 and 2) Mathematische Annalen, 1895 and 1897, Original in German. French traduction by Éditions Jacques Gabay

L. Cardelli, A semantics of multiple inheritance, Semantics of Data Types Full version in Information and Computation, pp.51-67138, 1984.
DOI : 10.1007/3-540-13346-1_2

L. Cardelli, Program fragments, linking, and modularization, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '97, pp.266-277, 1997.
DOI : 10.1145/263699.263735
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.8472

R. Chatterjee, B. G. Ryder, and W. A. Landi, Relevant context inference, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '99, pp.133-146, 1999.
DOI : 10.1145/292540.292554
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.6842

A. Church, An Unsolvable Problem of Elementary Number Theory, American Journal of Mathematics, vol.58, issue.2, pp.345-363, 1936.
DOI : 10.2307/2371045

R. Clarisó and J. Coradella, The octahedron abstract domain, Proceedings of the 11th Static Analysis Symposium (SAS'04), Lectures Notes in Computer Science, 2004.

M. Comini, G. Levi, and M. C. Meo, A Theory of Observables for Logic Programs, Information and Computation, vol.169, issue.1, pp.23-80, 2001.
DOI : 10.1006/inco.2000.3024

W. R. Cook, W. Hill, and P. S. Canning, Inheritance is not subtyping, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '90, 1990.
DOI : 10.1145/96709.96721

W. R. Cook and J. Palsberg, A Denotational Semantics of Inheritance and Its Correctness, Information and Computation, vol.114, issue.2, pp.329-350, 1994.
DOI : 10.1006/inco.1994.1090

P. Cousot, Asynchronous iterative methods for solving a fixed point system of monotone equations in a complete lattice, Res. rep. R.R. Laboratoire IMAG, vol.88, 1977.

P. Cousot, Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique de programmes, Thèse d'Etat ès sciences mathématiques, 1978.

P. Cousot, Types as abstract interpretations, invited paper, Proceedings of the 24th ACM Symposium on Principles of Programming Languages (POPL '97), pp.316-331, 1997.

P. Cousot, The calculational design of a generic abstract interpreter, Calculational System Design. NATO ASI Series F. IOS Press, 1999.

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.47-103, 2002.
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/inria-00528590

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, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '79, pp.269-282, 1979.
DOI : 10.1145/567752.567778

P. Cousot and R. Cousot, Relational abstract interpretation of higherorder functional programs, JTASPEFL '91, pp.33-36, 1991.

P. Cousot and R. Cousot, Abstract interpretation and application to logic programs, The Journal of Logic Programming, vol.13, issue.2-3, pp.2-3, 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, Modular Static Program Analysis, Proceedings of the Eleventh International Conference on Compiler Construction, pp.159-178, 2002.
DOI : 10.1007/3-540-45937-5_13

P. Cousot and R. Cousot, Systematic design of program transformation frameworks by abstract interpretation, Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '02), pp.178-190, 2002.

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-97, 1978.
DOI : 10.1145/512760.512770

O. Dahl and K. Nygaard, SIMULA: an ALGOL-based simulation language, Communications of the ACM, vol.9, issue.9, pp.671-678, 1966.
DOI : 10.1145/365813.365819

D. Distefano, J. P. Katoen, and A. Rensik, On a Temporal Logic for Object-Based Systems, 4th International Conference on Formal Methods for Open Object-Based Distributed Systems IFIP Conference Proceedings, pp.285-304, 2000.
DOI : 10.1093/logcom/5.5.603

K. Driesen and U. Hölzle, The direct cost of virtual function calls in C++, Proceedings of the 1996 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA '96) SIGPLAN Notices, pp.306-323, 1996.

M. Ernst, Summary of dynamically discovering likely program invariants, Proceedings IEEE International Conference on Software Maintenance. ICSM 2001, 2002.
DOI : 10.1109/ICSM.2001.972767

J. Feret, Abstract interpretation of mobile systems, The Journal of Logic and Algebraic Programming, vol.63, issue.1, 2004.
DOI : 10.1016/j.jlap.2004.01.005
URL : https://hal.archives-ouvertes.fr/inria-00527910

C. Flanagan, K. R. Leino, and E. Java, Houdini, an Annotation Assistant for ESC/Java, Proceedings of the International Symposium of Formal Methods Europe, pp.500-517, 2001.
DOI : 10.1007/3-540-45251-6_29
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.19.8640

C. Flanagan, K. R. Leino, M. Lillibridge, G. Nelson, J. B. Saxe et al., Extended static checking for Java, Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'02)48] Free Software Foundation. Nana: improved sup- port for assertions and logging. GNU, pp.234-245, 2002.

. Gartner and . Inc, NET vs Java: Competition or cooperation? Slides are available online at http

S. Genaim and M. Codish, Incremental refinement of semantic based program analysis for logic programs, Proceedings of the 22nd Australasian Computer Science Conference, 1999.

S. Ghemawat, K. H. Randall, and D. J. Scales, Field analysis: getting useful and low-cost interprocedural information, Proceedings of the 2000 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'00) ACM SIGPLAN Notices, pp.334-344, 2000.

R. Giacobazzi and F. Ranzato, Refining and compressing abstract domains, Proceedings of the International Colloquium on Automata, Languages and Programming (ICALP'97, pp.771-781, 1997.
DOI : 10.1007/3-540-63165-8_230
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.75.1515

R. Giacobazzi and F. Ranzato, The reduced relative power operation on abstract domains, Theoretical Computer Science, vol.216, issue.1-2, pp.159-211, 1999.
DOI : 10.1016/S0304-3975(98)00194-7
URL : http://doi.org/10.1016/s0304-3975(98)00194-7

R. Giacobazzi, F. Ranzato, and F. Scozzari, Making abstract interpretations complete, Journal of the ACM, vol.47, issue.2, pp.361-416, 2000.
DOI : 10.1145/333979.333989
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.2353

A. Goldberg and D. Robson, Smalltalk-80: The Language and Its Implementation, 1983.

J. Gosling, B. Joy, G. Steele, and G. Bracha, The Java Language Specification -2nd Edition, Sun Microsystems, 2001.

P. Granger, Static analysis of linear congruence equalities among variables of a program, Proceedings of the International Joint Conference on Theory and Practice of Software Development (TAPSOFT'91), pp.169-192, 1991.
DOI : 10.1007/3-540-53982-4_10

J. V. Guttag, S. J. Horning, J. J. Garland, K. D. Jones, A. Modet et al., Larch: Languages and Tools for Formal Specification. Texts and Monographs in Computer Science, 1993.

M. Handjieva and S. Tzolovski, Refining Static Analyses by Trace-Based Partitioning Using Control Flow, Proceedings of the 5th Static Analysis Symposium (SAS '98), volume 1503 of Lectures Notes in Computer Science, pp.200-215, 1998.
DOI : 10.1007/3-540-49727-7_12

M. Huisman, B. Jacobs, J. Van-den, and . Berg, A case study in class library verification: Java's vector class, Object-Oriented Technology: ECOOP'99 Workshop Reader, pp.109-110, 1999.

K. Huizing and R. Kuiper, Verification of Object Oriented Programs Using Class Invariants, Fundamental Approaches to Software Engineering , Third International Conference, pp.208-221, 2000.
DOI : 10.1007/3-540-46428-X_15

A. Igarashi, B. Pierce, and P. Wadler, Featherweight Java: a minimal core calculus for Java and GJ, 14th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA'99) ACM SIGPLAN Notices, pp.132-146, 1999.
DOI : 10.1145/503502.503505

B. Jacobs, J. Van-den-berg, H. Huismann, M. Van-berkum, U. Hensel et al., Reasoning about Java classes (preliminary report), 13th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA'98), 1998.

S. N. Kamin and U. S. Reddy, Two semantic models of object-oriented languages, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design, pp.464-495, 1994.

O. Kupferman and M. Y. Vardi, Modular Model Checking, Lectures Notes in Computer Science, vol.1536, pp.381-401, 1997.
DOI : 10.1007/3-540-49213-5_14

J. L. Lassez, M. J. Maher, and K. Marriott, Unification revisited, Foundations of Deductive Databases and Logic Programming, pp.587-625, 1988.
DOI : 10.1007/3-540-19129-1_4

G. T. Leavens, A. L. Baker, and C. Ruby, Preliminary design of JML, ACM SIGSOFT Software Engineering Notes, vol.31, issue.3, 2003.
DOI : 10.1145/1127878.1127884

G. T. Leavens and K. K. Dhara, Concepts of behavioral subtyping and a sketch of their extension to component-based systems, Foundations of Component- Based Systems, pp.113-135, 2000.

X. Leroy, A modular module system, Journal of Functional Programming, vol.10, issue.3, pp.269-303, 2000.
DOI : 10.1017/S0956796800003683
URL : https://hal.archives-ouvertes.fr/inria-00073825

X. Leroy, The Objective Caml system release 3.07, 2004.

J. Lewis and W. Loftus, Java Software Solutions, Second Edition Update, 2001.

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

B. H. Liskov and J. M. Wing, A behavioral notion of subtyping, ACM Transactions on Programming Languages and Systems, vol.16, issue.6, pp.1811-1841, 1994.
DOI : 10.1145/197320.197383

F. Logozzo, Class-Level Modular Analysis for Object Oriented Languages, Proceedings of the 10th Static Analysis Symposium 2003 (SAS '03), volume 2694 of Lectures Notes in Computer Science, pp.37-54, 2003.
DOI : 10.1007/3-540-44898-5_3

F. Logozzo, An Approach to Behavioral Subtyping Based on Static Analysis, Proceedings of the International Workshop on Test and Analysis of Component Based Systems Electronic Notes in Theoretical Computer Science, 2004.
DOI : 10.1016/j.entcs.2004.02.074

F. Logozzo, Approximating module semantics with constraints, Proceedings of the 2004 ACM symposium on Applied computing , SAC '04, pp.1490-1495, 2004.
DOI : 10.1145/967900.968197
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.58.321

F. Logozzo, Automatic Inference of Class Invariants, Proceedings of the 5th International Conference on Verification, pp.211-222, 2004.
DOI : 10.1007/978-3-540-24622-0_18
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.2.5821

F. Logozzo, Separate compositional analysis of class-based objectoriented languages, Proceedings of the 10th International Conference on Algebraic Methodology And Software Technology, pp.332-346, 2004.

L. Mauborgne, Abstract interpretation using typed decision graphs, Science of Computer Programming, vol.31, issue.1, pp.91-112, 1998.
DOI : 10.1016/S0167-6423(96)00042-1
URL : http://doi.org/10.1016/s0167-6423(96)00042-1

B. Meyer, Eiffel: The Language, 1992.

B. Meyer, Object-Oriented Software Construction Professional Technical Reference, 1997.

M. Inc, The Component Object Model Specification. Microsoft, 2003.

]. A. Miné, The octagon abstract domain, AST, pp.310-319, 2001.

E. Noether, Idealtheorie in Ringbereichen, Mathematische Annalen, vol.150, issue.1-2, pp.24-66, 1921.
DOI : 10.1007/BF01464225

T. Owen and D. Watson, Reducing the Cost of Object Boxing, Proceedings of the 13th International Conference on Compiler Construction, pp.202-216, 2004.
DOI : 10.1007/978-3-540-24723-4_14

J. Palsberg and M. I. Schwartzbach, Object-Oriented Type Systems, 1994.

F. Pessaux and X. Leroy, Type-based analysis of uncaught exceptions, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '99, pp.340-377, 2000.
DOI : 10.1145/292540.292565
URL : https://hal.archives-ouvertes.fr/hal-01499959

I. Pollet, B. L. Charlier, and A. Cortesi, Distinctness and Sharing Domains for Static Analysis of Java Programs, Proceedings of the European Conference on Object Oriented Programming, pp.77-98, 2001.
DOI : 10.1007/3-540-45337-7_5

C. Probst, Modular Control Flow Analysis for Libraries, Proceedings of the 9th Static Analysys Symposium (SAS '02), volume 2477 of Lecture Notes in Computer Science, pp.165-179, 2002.
DOI : 10.1007/3-540-45789-5_14

S. Qadeer, S. K. Rajamani, and J. Rehof, Summarizing procedures in concurrent programs, Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.245-255, 2004.
DOI : 10.1145/964001.964022
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.116.5357

G. Ramalingam, A. Warshavsky, J. Field, D. Goyal, and M. Sagiv, Deriving specialized program analyses for certifying component-client conformance, ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI '02) ACM SIGPLAN Notices, pp.83-94, 2002.
DOI : 10.1145/512529.512540
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.12.2395

A. Rountev, A. Milanova, and B. G. Ryder, Fragment class analysis for testing of polymorphism in Java software, Proceedings of the 25th International Conference on Software Engineering (ICSE'03), pp.210-220, 2003.

J. Rumbaugh, I. Jacobson, and G. Booch, The Unified Modeling Language Reference Manual, 1999.

D. S. Scott, Domains for denotational semantics, Proceedings of 9th International Colloquium on Automata, Languages and Programming (ICALP'82), pp.577-613, 1982.
DOI : 10.1007/BFb0012801

F. Spoto and T. P. Jensen, Class analyses as abstract interpretations of trace semantics, ACM Transactions on Programming Languages and Systems, vol.25, issue.5, pp.578-630, 2003.
DOI : 10.1145/937563.937565

R. Stärk, J. Schmid, and E. Börger, Java and the JavaVirtual Machine: Definition, Verification, Validation, 2001.

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
URL : http://projecteuclid.org/download/pdf_1/euclid.pjm/1103044538

K. Zee and M. Rinard, Write barrier removal by static analysis, 17th Annual ACM Conference on Object-Oriented Programming, Systems , Languages and Applications (OOPSLA '02) SIGPLAN Notices, pp.191-210, 2002.
DOI : 10.1145/582419.582439
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.133.7327