Model Checking C Programs by Translating C to Promela

Abstract: Nowadays, the cost of program errors is increasing from day to day, so software reliability becomes a critical problem to the whole world. C is one of the most popular programming languages, and has been widely used for developing all types of software. Hence, the security of software written in C accounts for an important proportion of software reliability. Spin model checker is the world's most popular tool for detecting software defects in concurrent system designs. However, it could not check C programs directly. This thesis will describe a mediate method of model checking C codes to find potential problems in concurrent programs and parallel systems using Spin. We hope it could initiate more study in this new method for model checking C and other languages. The translator we developed for this thesis uses syntax-directed translation techniques for doing the translations, and several tools and languages are involved. OCaml is the language we used for programming. CIL is the carrier and does the C syntax analysis for our translator. Spin model checker is the tool for checking the translations. C is the input language, and Promela is the target output language.