The evolution of formal methods allowed us to overcome many obstacles
in verification of procedural programs. However, wide spreading of object-oriented
languages has brought new challenges, even in the case of sequential programs.
These problems were thoroughly examined by ESC/Java and Spec# teams in their
papers [10, 12], though in...