The problems of C program verification

The fully automatic verification of programs is a tempting and hardly accessible goal of modern programming. The low-level nature of the most popular programming languages, such as C and C+, has raised its difficulty to a new level. New formal methods and specification languages are required, because the classical Hoare approach and first-level logics are no more adequate for the task. This paper has two aims. First, it gives an overview of the two-level approach to verification of C-light programs and, second, it describes the successful application of this method to verification of so called “verification challenges”. An interface with the theorem provers Simplify and Z3 is presented when discussing the proof of verification conditions.