Two-level mixed verification method of C-light programs in terms of safety logic

In this paper, a formalization of the two-level mixed verification method of C-light programs, based on program specific transition systems, is suggested. Two kinds of such systems are used to formalize the method. The first kind, operational semantics specific transition systems, is used to specify the C-light mixed operational semantics. The second kind, safety logic specific transition systems, is used to specify the mixed axiomatic semantics of C-kernel into which C-light programs are translated. The formalization makes this method more technological.