Error-tracing axiomatic semantics for C-kernel

The classical Hoare logic links separate verification conditions (VCs) to linear paths of a program. The real verification condition generators (VCG) link VCs to line numbers at best. It can be insufficient, since VCs contain information neither about the evaluation order nor about correspondence between their fragments and specific operations. Verification of complex programs is inevitably confronted by difficulties of VC interpretation and error localization. This paper describes an extension of axiomatic semantics of the C-kernel language. The extended calculus will be able to derive VCs accompanied with formal derivation protocols useful in VC understanding and error tracing.