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...
This paper describes a new approach to the analysis and verification of imperative programs, which allows us to integrate, unify and combine the methods and techniques of analysis and verification of imperative programs, accumulate and use knowledge about them. A feature of the approach is to use the domain-specific language...
Development of the C-light verification system is accompanied by various case studies. We have already demonstrated the applicability of our system to some examples from verification competitions. Those programs are connected to verification-difficult issues but, as a rule, they are represented by artificial or trivial pieces of code. Now we...