Automatic C Program Verification Based on Mixed Axiomatic Semantics

Modelirovanie i Analiz Informacionnyh Sistem

A. V. Promsky¹  D. A. Kondratyev²  I. V. Maryasov³  V. A. Nepomnyaschy³ 

[1] Новосибирский государственный университет;Институт систем информатики им. А. П. Ершова СО РАН,;Институт систем информатики им. А. П. Ершова СО РАН;

关键词: верификация;    операционная семантика;    аксиоматическая семантика;    язык C;    язык C-light;    язык C-kernel;    частичная корректность;    ACSL;    LLVM;    Simplify;   

DOI  :  

来源: DOAJ

【 摘 要 】

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.

【 授权许可】

Unknown