|
Article information
2017 , Volume 22, Special issue, p.44-59
Kondratyev D.A.
The extension of the C-light project using symbolic verification method of definite iterations
The project for deductive verification of C programs is being developed in the Laboratory of theoretical programming, IIS SB RAS. One of the goals of this project is development of an extendable self-applicable verification condition generator for the C language. The MetaVCG approach was chosen to achieve this purpose. The metagenerator utilizes axiomatic semantics in a special format and automatically produces the verification condition generator. The correctness and completeness of MetaVCG are ensured by using only strongly limited axiomatic semantics as the argument of metagenerator. The metageneration idea allows the C-light verification system to be supplemented with the semantic mark-up method. It focuses on such problems as the analysis, tracing and explanation of verification conditions. This concept contains such definition of Hoare rules extension by semantic labels, that calculus itself can be used to generate explanations of verification conditions. The error localization experiments were successfully performed. The symbolic method of verifying for-loops that have the statement of assignment to array elements as the loop body is based on the replacement operation. It represents the loop effect in a symbolic form and allows the proof rule to be created for these loops without invariants. The MetaVCG approach allows the C-light system to be easily supplementing with such rules and new concepts of semantic labels. The application of C-light system to the verification of linear algebra programs is explained in this article. The MetaVCG approach allows special set of inference rules to be used for verifying such programs.
[full text]
Keywords: verification, MetaVCG, symbolic method of verification, definite iterations, verification condition, semantic mark-up method
Author(s):
Kondratyev Dmitry Aleksandrovich
Position: Junior Research Scientist
Office: A.P. Ershov Institute of Informatics Systems Siberian Branch of the Russian Academy of Sciences
Address: 630090, Russia, Novosibirsk, 6, Acad. Lavrentyev pr.
E-mail: apple-66@mail.ru
SPIN-code: 4318-8908 References:
[1] Nepomniaschy, V.A., Anureev, I.S., Mikhaylov, I.N., Promskiy, A.V. Orientirovannyy na verifikatsiyu yazyk C-light. Sistemnaya informatika: Sbornik nauchnych trudov [Verification oriented language C-light]. In-t sistem informatiki RAN; 2004; (9):51–134. (In Russ.)
[2] Moriconi, M., Schwarts, R.L. Automatic Construction of Verification Condition Generators From Hoare Logics. Lecture Notes in Computer Science. 1981; (115):363–377.
[3] Kondratyev, D.A., Promskiy, A.V. Developing a Self Applicable Verification System. Theory and Practices. Automatic Control and Computer Sciences. 2015; 49(7):445–452.
[4] Nepomniaschy, V.A. Symbolic method of verification of definite iterations over altered data structures. Programming and Computer Software. 2005; 31(1):1–9.
[5] Apt, K.R., Olderog, E.R. Verification of sequential and concurrent programs. Berlin: Springer-Verlag; 1991: 450.
[6] Nepomniaschy, V.A., Sulimov, A.A. Verification of linear algebra programs in the SPECTRUM system. Cybernetics and system analysis. 1992; (5):136–144. (In Russ.)
[7] Nepomniaschy, V.A., Ryakin, Î.Ì. Prikladnye metody verifikatsii program [Applied methods of program verification]. Moscow: Radio i svyaz'. 1988: 256. (In Russ.)
[8] Denney, E., Fischer, B. Explaining Verification Conditions. Lecture Notes in Computer Science. Berlin: Springer-Verlag; 2008; (5140):145–159.
[9] Kondratyev, D.A. The extension of the MetaVCG approach by semantic mark-up concept. Proceedings of the International workshop-conference “Tools & Methods of Program Analysis”. Sankt-Peterburg: Izdatel'stvo Politekhnicheskogo universiteta; 2015:107–118. (In Russ.)
[10] Filliatre, J.C., March´e, C. Multi-prover verification of C programs. Lecture Notes in Computer Science. Berlin: Springer-Verlag; 2004; (3308):15–29.
[11] Cohen, E., Dahlweid, M., Hillebrand, M.A., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S. VCC: A Practical System for Verifying Concurrent C. Lecture Notes in Computer Science. Berlin: Springer-Verlag; 2009: (5674):23–42.
Bibliography link:
Kondratyev D.A. The extension of the C-light project using symbolic verification method of definite iterations // Computational technologies. 2017. V. 22. XVII All-Russian Conference of Young Scientists on Mathematical Modeling and Information Technology. P. 44-59
|
