maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2017-6-743-754mais-611Research ArticleОригинальные статьиArticlesЭлиминация инвариантов финитных итераций над массивами при верификации Си программInvariant Elimination of Definite Iterations over Arrays in C Programs Verificationhttps://orcid.org/0000-0002-2497-6484МарьясовИлья ВладимировичMaryasovIlya V.

канд. физ.-мат. наук

PhD

ivm@iis.nsk.suhttps://orcid.org/0000-0003-1364-5281НепомнящийВалерий АлександровичNepomniaschyValery A.

канд. физ.-мат. наук

PhD

vnep@iis.nsk.suhttps://orcid.org/0000-0002-9387-6735КондратьевДмитрий АлександровичKondratyevDmitry A.

аспирант

postgraduate student

apple-66@mail.ruИнститут систем информатики им. А. П. Ершова СО РАНРоссияA. P. Ershov Institute of Informatics Systems SB RASRussian Federation201718122017246743745Copyright © Марьясов И.В., Непомнящий В.А., Кондратьев Д.А., 20172017Марьясов И.В., Непомнящий В.А., Кондратьев Д.А.Maryasov I.V., Nepomniaschy V.A., Kondratyev D.A.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/611

Данная работа представляет дальнейшее развитие метода верификации финитной итерации [7]. Он расширяет метод смешанной аксиоматической семантики [1], предложенный для верификации C-light программ. Это расширение включает метод верификации для финитной итерации над неизменяемыми массивами с выходом из цикла в C-light программах. Метод содержит правило вывода для итерации без инвариантов, которое использует специальную функцию, выражающую действие тела цикла. Данное правило было реализовано в генераторе условий корректности, являющемся частью нашей системы верификации C-light программ. Для доказательства порождённых условий корректности применяется метод математической индукции, вызывающий сложности у SMT-решателей. В нашей системе верификации на стадии доказательства используется SMT-решатель CVC4. Для преодоления упомянутой трудности применяется стратегия переписывания условий корректности. Для доказательства условий корректности предложен метод, основанный на расширении теории новыми теоремами. Рассмотрен пример, иллюстрирующий применение данных методов. Статья публикуется в авторской редакции.

 

This work represents the further development of the method for definite iteration verification [7]. It extends the mixed axiomatic semantics method [1] suggested for C-light program verification. This extension includes a verification method for definite iteration over unchangeable arrays with a loop exit in C-light programs. The method includes an inference rule for the iteration without invariants, which uses a special function that expresses loop body. This rule was implemented in verification conditions generator, which is the part of our C-light verification system. To prove generated verification conditions an induction is applied which is a challenge for SMT-solvers. At proof stage the SMT-solver CVC4 is used in our verification system. To overcome mentioned difficulty a rewriting strategy for verification conditions is suggested. A method based on theory extension by new theorems to prove verification conditions is suggested. An example, which illustrates the application of these methods, is considered. The article is published in the authors’ wording.

 

C-lightСиинварианты цикловсмешанная аксиоматическая семантикафинитная итерациямассивыCVC4спецификацияверификациялогика ХоараC-lightloop invariantsmixed axiomatic semanticsdefinite iterationarraysCVC4specificationverificationHoare logicReferencesI. S. Anureev, I. V. Maryasov, V. A. Nepomniaschy, “C-programs Verification Based on Mixed Axiomatic Semantics”, Automatic Control and Computer Sciences, 45:7 (2011), 485–500.I. S. Anureev, I. V. Maryasov, V. A. Nepomniaschy, “C-programs Verification Based on Mixed Axiomatic Semantics”, Automatic Control and Computer Sciences, 45:7 (2011), 485–500.C. Barrett, C. L., Conway, M. Deters, L. Hadarean, D. Jovanovi´c, T. King, A. Reynolds, C. Tinelli, “CVC4”, 23rd Int. Conf. CAV, Lecture Notes in Computer Science, 6806 (2011), 171–177.C. Barrett, C. L., Conway, M. Deters, L. Hadarean, D. Jovanovi´c, T. King, A. Reynolds, C. Tinelli, “CVC4”, 23rd Int. Conf. CAV, Lecture Notes in Computer Science, 6806 (2011), 171–177.E. Cohen, M. Dahlweid, M. Hillebrand, D. Leinenbach, M. Moskal, T. Santen, W. Schulte,S. Tobies, “VCC: A Practical System for Verifying Concurrent C”, 22nd Int. Conf.TPHOLs, Lecture Notes in Computer Science, 5674 (2009), 23–42.E. Cohen, M. Dahlweid, M. Hillebrand, D. Leinenbach, M. Moskal, T. Santen, W. Schulte,S. Tobies, “VCC: A Practical System for Verifying Concurrent C”, 22nd Int. Conf.TPHOLs, Lecture Notes in Computer Science, 5674 (2009), 23–42.J.-C. Filli˄atre, C. March´e, “Multi-prover Verification of C Programs”, 6th ICFEM, Lecture Notes in Computer Science, 3308 (2004), 15–29.J.-C. Filli˄atre, C. March´e, “Multi-prover Verification of C Programs”, 6th ICFEM, Lecture Notes in Computer Science, 3308 (2004), 15–29.D. A. Kondratyev, “The Extension of the MetaVCG Approach by Semantic Mark-up Concept”, Int. Workshop-conf. ”Tools & Methods of Program Analysis”, St. Petersburg, 2015, 107–118.D. A. Kondratyev, “The Extension of the MetaVCG Approach by Semantic Mark-up Concept”, Int. Workshop-conf. ”Tools & Methods of Program Analysis”, St. Petersburg, 2015, 107–118.K. R. M. Leino, “Automating Induction with an SMT Solver”, 13th Int. Conf. VMCAI, Lecture Notes in Computer Science, 7148 (2012), 315–331.K. R. M. Leino, “Automating Induction with an SMT Solver”, 13th Int. Conf. VMCAI, Lecture Notes in Computer Science, 7148 (2012), 315–331.I. V. Maryasov, V. A. Nepomniaschy, “Loop Invariants Elimination for Definite Iterations over Unchangeable Data Structures in C Programs”, Modeling and Analysis of Information Systems, 22:6 (2015), 773–782.I. V. Maryasov, V. A. Nepomniaschy, “Loop Invariants Elimination for Definite Iterations over Unchangeable Data Structures in C Programs”, Modeling and Analysis of Information Systems, 22:6 (2015), 773–782.I. V. Maryasov, V. A. Nepomniaschy, D. A. Kondratyev, “Verification of Definite Iteration over Arrays with a Loop Exit in C Programs”, System Informatics, 2017, š 10, 57–66.I. V. Maryasov, V. A. Nepomniaschy, D. A. Kondratyev, “Verification of Definite Iteration over Arrays with a Loop Exit in C Programs”, System Informatics, 2017, š 10, 57–66.I. V. Maryasov, V. A. Nepomniaschy, A. V. Promsky, D. A. Kondratyev, “Automatic C Program Verification Based on Mixed Axiomatic Semantics”, Automatic Control and Computer Sciences, 48:7 (2014), 407–414.I. V. Maryasov, V. A. Nepomniaschy, A. V. Promsky, D. A. Kondratyev, “Automatic C Program Verification Based on Mixed Axiomatic Semantics”, Automatic Control and Computer Sciences, 48:7 (2014), 407–414.M. Moriconi, R. L. Schwarts, “Automatic Construction of Verification Condition Generators From Hoare Logics”, Automata, Languages and Programming, Lecture Notes in Computer Science, 115 (1981), 363–377.M. Moriconi, R. L. Schwarts, “Automatic Construction of Verification Condition Generators From Hoare Logics”, Automata, Languages and Programming, Lecture Notes in Computer Science, 115 (1981), 363–377.V. A. Nepomniaschy, “Verification of Definite Iteration over Hierarchical Data Structures”, FASE/ ETAPS, Lecture Notes in Computer Science, 1577 (1999), 176–187.V. A. Nepomniaschy, “Verification of Definite Iteration over Hierarchical Data Structures”, FASE/ ETAPS, Lecture Notes in Computer Science, 1577 (1999), 176–187.A. Reynolds, V. Kuncak, “Induction for SMT solvers”, 16th Int. Conf. VMCAI, Lecture Notes in Computer Science, 8931 (2015), 80–98.A. Reynolds, V. Kuncak, “Induction for SMT solvers”, 16th Int. Conf. VMCAI, Lecture Notes in Computer Science, 8931 (2015), 80–98.T. Tuerk, “Local Reasoning about While-Loops”, VSTTE, 2010, 29–39.T. Tuerk, “Local Reasoning about While-Loops”, VSTTE, 2010, 29–39.

The authors declare that there are no conflicts of interest present.