Experiments on self-applicability in the C-light verification system. Part 2

Successful development of the theoretical foundations of C program verification in the project C-light allowed us to address an interesting practical task. We would like to develop a self-applicable verification system for C programs. The first step towards this goal was a series of experiments to verify some fragments of the input analyzer/translator. Now we are ready to address the verification condition generator. As a basis of our approach, we chose the metageneration approach proposed by Moriconi and Schwartz. Metageneration allows us to build automatically a recursively defined generator from a Hoare logic and also ensures its consistency and completeness. This paper discusses the metageneration approach as well as the experiments to verify its implementation in C-light.