Towards Verification of C Programs. C-Light Language and Its Formal Semantics. - Valery A. Nepomniaschy; Igor S. Anureev; I. N. Mikhailov; Alexey V. Promsky (Program. Comput. Softw., 2002)