Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1109/CSCloud.2016.30 | 2016 IEEE 3rd International Conference on Cyber Security and Cloud Computing (CSCloud) |
Keywords | Field | DocType |
code correctness verification,theorem proving,VCC,real-time operating system | Data structure,Data modeling,Programming language,Computer science,Scheduling (computing),Correctness,Automated theorem proving,Real-time operating system,Software,Formal verification | Conference |
ISBN | Citations | PageRank |
978-1-5090-0947-3 | 0 | 0.34 |
References | Authors | |
6 | 6 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Hongliang Liang | 1 | 26 | 12.76 |
| Daijie Zhang | 2 | 2 | 0.71 |
| Xiaoxiao Pei | 3 | 16 | 2.07 |
| Xiaodong Jia | 4 | 0 | 0.34 |
| Guangyuan Li | 5 | 56 | 7.19 |
| Jiuyun Xu | 6 | 78 | 11.50 |