Automatic C Program Verification Based on Mixed Axiomatic Semantics - I. V. Maryasov; V. A. Nepomnyaschy; A. V. Promsky; D. A. Kondratyev (Моделирование и анализ информационных систем, 2013)
The development of the C-light project resulted in the application of new formalisms and implementation techniques which facilitate the verification process. The mixed axiomatic semantics proposes a choice between simplified and full-strength deduction rules depending on program objects and their properties. The LLVM infrastructure helps greatly in writing the C-light program analyzer and translator. The semantical labeling technique, proposed earlier, can now be safely kept in verification conditions during their proof. Two programs from the well-known verification benchmarks illustrate the applicability of the system.