Two lines of developing the C program verification project at the A.P. Ershov Institute of Informatic Systems are presented. Firstly, the axiomatic semantics of the C-kernel language was extended by the semantic labelling. The labels introduced in the Hoare calculus correspond to various concepts inherent in verification conditions (VC). These labels can be extracted from terms and rendered into explanations written in the natural language. User friendly explanations can play a crucial role in VC understanding and error localization. Secondly, a subset of the C standard library was specified. The specifications written in ACSL correspond to the C-light memory model. Examples illustrating the use of the proposed techniques are presented.