The C#-light project: solution of some verification challenges

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 many cases they just state the presence of the challenge. This paper presents an overview of some problematic issues and a three-level approach to their solution in the C#-light project.