C-programs Verification on Basis of Mixed Axiomatic Semantics
Igor Sergeevich Anureev, I. V. Maryasov, Valery A. Nepomniaschy · DOAJ (DOAJ: Directory of Open Access Journals) · 2010
The mixed axiomatic semantics of a C-kernel language is described. This language is the kernel of a representative C language subset which is callexl 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.