Abstract

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.

DOI
10.31144/bncc.cs.2542-1972.2014.n37.p93-105
File
promsky.pdf169.41 KB
Issue
Pages
93-105