A three-stage method of C program verification

A three-stage method of C program verification is presented. It is a further development of the two-stage method in the framework of the C-light project. An additional stage of normalization of C-light programs is introduced and optimization of the two-stage method caused by this introduction is considered.