Experiments on self-applicability in the C-light verification system

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 can address the more realistic tests. The first series of experiments is based on fragments of the input analyzer/translator of the C-light system. The trials include axiomatization of problematic domains in the prover Simplify, the development of ACSL annotations and inductive reuse of already specified standard library routines. Thus the first step to a self-applicable C program verification system has been taken.