A three-level approach to C# program verification

A new three-level approach to sequential object-oriented program verification is presented. It is applied to a significant С# subset called C#-light that includes all principal sequential С# constructs. At the first stage, C#-light is translated into an intermediate language C#-kernel that allows us to simplify axiomatic semantics. At the second stage, lazy verification conditions are generated by means of backward rules of axiomatic C#-kernel semantics. Lazy verification conditions can include special functional symbols which are refined at the third stage. An example of verification of a C#-light program serves to illustrate this three-level approach.