C-programs verification on basis of mixed axiomatic semantics

The mixed axiomatic semantics of a C-kernel language is described. This language is the kernel of a representative C language subset which is called C-light. Such semantics allows to simplify the verification conditions in many cases. This semantics is a base of verification conditions generator of C-kernel programs. An example which illustrates the use of inference rules of the semantics is considered.