TWO-LEVEL MIXED VERIFICATION METHOD OF C-LIGHT PROGRAMS IN TERMS OF SAFETY LOGIC
Igor Sergeevich Anureev, I. V. Maryasov, Valery A. Nepomniaschy · Bulletin of the Novosibirsk Computing Center Series Computer Science · 2012
In this paper, a formalization of the two-level mixed verication method of C-light programs, based on program specic transition systems, is suggested.Two kinds of such systems are used to formalize the method.The rst kind, operational semantics specic transition systems, is used to specify the C-light mixed operational semantics.The second kind, safety logic specic 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.