D. Cachera, T. P. Jensen, D. Pichardie, and V. Rusu, Extracting a data flow analyser in constructive logic, Theoretical Computer Science, vol.342, issue.1, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00564633

P. Chalin and P. R. James, Non-null References by Default in Java: Alleviating the Nullity Annotation Burden, Proceedings of European Conference on Object- Oriented Programming
DOI : 10.1007/978-3-540-73589-2_12

M. Cielecki, J. Fulara, K. Jakubczyk, and L. Jancewicz, Propagation of JML non-null annotations in Java programs, Proceedings of the 4th international symposium on Principles and practice of programming in Java , PPPJ '06
DOI : 10.1145/1168054.1168073

M. Das, S. Lerner, and M. Seigle, Esp: path-sensitive program verification in polynomial time, Proceedings of the ACM SIGPLAN Conference on Programming language design and implementation (PLDI'02)

T. Ekman and G. Hedin, Pluggable non-null types for Java, Extensible Compiler Construction, chapter, 2006.

M. Fähndrich and K. R. Leino, Declaring and checking non-null types in an object-oriented language, Proceedings of Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA'03)

M. Fähndrich and S. Xia, Establishing object invariants with delayed types, OOPSLA '07: Proceedings of the 22nd ACM conference on Object Oriented Programming Systems and Applications

C. Flanagan, K. R. Leino, and E. Java, Houdini, an annotation assistant for, Proceedings of International Symposium of Formal Methods Europe (FME'01)

S. N. Freund and J. C. Mitchell, A formal framework for the java bytecode language and verifier, Proceedings of the 14th ACM conference on Object-oriented programming, systems, languages, and applications (OOPSLA '99)

D. Hovemeyer and W. Pugh, Finding more null pointer bugs, but not too many, Proceedings of the 7th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering , PASTE '07
DOI : 10.1145/1251535.1251537
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.93.1704

D. Hovemeyer, J. Spacco, and W. Pugh, Evaluating and tuning a static analysis to find null pointer bugs, SIGSOFT Softw. Eng. Notes, issue.1, p.31, 2006.

M. Kawahito, H. Komatsu, and T. Nakatani, Effective null pointer check elimination utilizing hardware trap, SIGPLAN Not, vol.35, issue.11, 2000.

. Proof, We denote in this proof L (m, i) by L and T (m, i) by T . We propose an induction on e

?. If-e-=-x-then and ?. , L(x) We distinguish two cases. ? If L (x) = Raw(super(C)), as Raw(C) Raw(super, Raw(C) L(x) holds ? otherwise L (x) L(x) holds by definition of L

@. If and ?. , Raw(C) and class(f ) C, then ?, L e .f : MayBeNull and

@. If and ?. , Raw(C) and C class(f ), then ?, L e .f : ? [f ] and

C. , H. , and T. Raw, The analysis gives us

. Proof, We do a case analysis on P m [i]

?. If-e-=-e, m,i),L (m,i) holds. We distinguish two cases. ? If e = MayBeNull, then it contradicts ?, L e : ? . So e = MayBeNull, so safe expr (e), L (m,i) holds

. Proof, ?. R. Is-lf-typable-w, L. , F. Pm, H. et al., ? means that there exists L and F such that

?. If and P. , we must show that safe expr (e) C,H ,T (m,i),L (m,i) holds. By hypothesis, ?, L e : ? , so from Lemma 26 the property holds

?. If and P. , we must show that L(m, i)(x) = MayBeNull and safe expr (e) C,H ,T (m,i),L (m,i) hold. By hypothesis, L(m, i)(x) = MayBeNull and ?, L e : ? , so, pp.55-81

?. If and P. , e j ), we must show that ?j, safe expr (e j ) class(m),H ,T (m,i),L (m,i) By hypothesis, ?i, ?? i , ?, L e i : ? i ), so, from Lemma 26, the property holds

?. If and P. , we must show that L (m, i)(x) = MayBeNull and f orallj, safe expr (e j ) class(m),H ,T (m,i),L (m,i) By hypothesis, (?i, ?, L e i : ? i ) and if ? [lookup(ms)] = [? ]? ? void then ?, L x : if ? ? Val then ? else Raw(super(C )) and ? = MayBeNull

M. , H. , T. , M. , H. et al., If P is LF-typable w.r.t. ?, L, F, then there exists, Theorem 5

. Proof, H. Let-(-m, T. , L. , L. et al., Forall m and m , let ?

?. By, class(m ) M (m )[this] holds