Automatic C program verification based on mixed axiomatic semantics
I. V. Maryasov, V. A. Nepomnyaschy, A. V. Promsky, Dmitry Alexandrovich Kondratyev · Automatic Control and Computer Sciences · 2014
The development of the C-light project led to the application of new formalisms and method implementations that facilitate the verification of C programs. The mixed axiomatic semantics provides a choice between simplified and general inference rules of verification conditions (VC) depending on the program objects and their properties. The LLVM infrastructure greatly simplifies the implementation of the analyzer and translator of C-light programs. The semantic labeling method proposed earlier can now be safely used in verification conditions during their proving. A program from well-known verification competition is considered in order to illustrate the applicability of the system.