Invited talk at 2nd International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2011)