EXPERIMENTS ON SELF-APPLICABILITY IN THE C-LIGHT VERIFICATION SYSTEM
A. V. Promsky · Bulletin of the Novosibirsk Computing Center Series Computer Science · 2013
Development of the C-light verication system is accompanied by various case studies.We have already demonstrated the applicability of our system to some examples from verication competitions.Those programs are connected to verication-dicult issues but, as a rule, they are represented by articial or trivial pieces of code.Now we can address the more realistic tests.The rst 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 specied standard library routines.Thus the rst step to a self-applicable C program verication system has been taken.