Aliasing in object-oriented programming. Types, analysis and verification.