Automatic C Program Verification Based on Mixed Axiomatic Semantics

Abstract

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.

Keywords

• program verification
• operational semantics
• axiomatic semantics
• c
• c-light
• c-kernel
• partial correctness
• acsl
• llvm
• simplify