A Correctness Verification Method for C Programs Based on VCC

The correctness of implementation codes is important especially for safety-critical software usually written in C programming language. We present a correctness verification method (CVM for short) for C codes based on an automatic theorem proving tool-VCC, and propose a specification simplification method to im-prove the correctness and readability of verification specification codes. Using CVM method, the scheduling module of a real-time operating system FreeRTOS6.1.1 is verified, which shows the feasibility and effectiveness when CVM method is applied to the real production software. Experiments show that the CVM method is feasible and effective in verifying the correctness the C codes, and the specification simplification method is also effective.