maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2013-6-52-63mais-157Research ArticleОригинальные статьиArticlesАвтоматическая верификация C-программ на основе смешанной аксиоматической семантикиAutomatic C Program Verification Based on Mixed Axiomatic SemanticsМарьясовИлья ВладимировичMaryasovI. V.

младший научный сотрудник,

630090, г. Новосибирск, пр. Лаврентьева, 6

младший научный сотрудник,

prospect Akademika Lavrentjeva, 6, Novosibirsk, 630090, Russia

ivm@iis.nsk.suНепомнящийВалерий АлександровичNepomnyaschyV. A.

зав. лабораторией,

630090, г. Новосибирск, пр. Лаврентьева, 6;

доцент,

630090, г. Новосибирск, ул. Пирогова, д. 2

зав. лабораторией,

prospect Akademika Lavrentjeva, 6, Novosibirsk, 630090, Russia;

доцент,

Pirogova Str., 2, Novosibirsk, 630090, Russia

vnep@iis.nsk.suПромскийАлексей ВладимировичPromskyA. V.

научный сотрудник,

630090, г. Новосибирск, пр. Лаврентьева, 6

научный сотрудник,

prospect Akademika Lavrentjeva, 6, Novosibirsk, 630090, Russia

promsky@iis.nsk.suКондратьевДмитрий АлександровичKondratyevD. A.

студент,

630090, г. Новосибирск, ул. Пирогова, д. 2

студент,

Pirogova Str., 2, Novosibirsk, 630090, Russia

apple-66@mail.ruИнститут систем информатики им. А. П. Ершова СО РАНРоссияA.P. Ershov Institute of Informatics Systems SB RASRussian FederationИнститут систем информатики им. А. П. Ершова СО РАН; Новосибирский государственный университетРоссияA.P. Ershov Institute of Informatics Systems SB RAS; Novosibirsk State UniversityRussian FederationИнститут систем информатики им. А. П. Ершова СО РАН,РоссияA.P. Ershov Institute of Informatics Systems SB RASRussian FederationНовосибирский государственный университетРоссияNovosibirsk State UniversityRussian Federation2013201220132065263Copyright © Марьясов И.В., Непомнящий В.А., Промский А.В., Кондратьев Д.А., 20132013Марьясов И.В., Непомнящий В.А., Промский А.В., Кондратьев Д.А.Maryasov I.V., Nepomnyaschy V.A., Promsky A.V., 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/157

Развитие проекта C-light привело к применению новых формализмов и реализации методов, которые облегчают процесс верификации С-программ. Смешанная аксиоматическая семантика предлагает выбор между упрощенными и общими правилами вывода условий корректности (УК) в зависимости от программных объектов и их свойств. Инфраструктура LLVM значительно упрощает реализацию анализатора и транслятора C-light программ. Метод семантических меток, предложенный ранее, теперь может быть безопасно исполь- зован в условиях корректности при их доказательстве. Рассмотрен пример из соревнования по верификации, иллюстрирующий применение нашей системы.

The development of the C-light project resulted in the application of new formalisms and implementation techniques which facilitate the verification process. The mixed axiomatic semantics proposes a choice between simplified and full-strength deduction rules depending on program objects and their properties. The LLVM infrastructure helps greatly in writing the C-light program analyzer and translator. The semantical labeling technique, proposed earlier, can now be safely kept in verification conditions during their proof. Two programs from the well-known verification benchmarks illustrate the applicability of the system.

верификацияоперационная семантикааксиоматическая семантикаязык Cязык C-lightязык C-kernelчастичная корректностьACSLLLVMSimplifyprogram verificationoperational semanticsaxiomatic semanticsCC-lightC-kernelpartial correctnessACSLLLVMSimplifyРФФИReferencesGamma E., Helm R., Johnson R., Vlissides J. Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, 1994. 395 p.Gamma E., Helm R., Johnson R., Vlissides J. Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, 1994. 395 p.Кондратьев Д. А., Промский А. В. Комплексный подход к локализации ошибок при верификации Си-программ // Системная информатика. 2013. № 1. С. 79–96 (Kondratyev D.A., Promsky A.V. Kompleksny podkhod k lokalizatsii oshibok pri verifikatsii Si-programm // Sistemnaya informatika. 2013. N 1. P. 79–96 [in Russian]).Кондратьев Д. А., Промский А. В. Комплексный подход к локализации ошибок при верификации Си-программ // Системная информатика. 2013. № 1. С. 79–96 (Kondratyev D.A., Promsky A.V. Kompleksny podkhod k lokalizatsii oshibok pri verifikatsii Si-programm // Sistemnaya informatika. 2013. N 1. P. 79–96 [in Russian]).Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. Ориентированный на верификацию язык C-light // Системная информатика: сборник научных трудов. Новосибирск: Издательство СО РАН. 2004. Вып. 9: Формальные методы и модели информатики. С. 51 – 134 (Nepomnyaschy V.A., Anureev I.S., Mikhaylov I.N., Promsky A.V. Orientirovanny na verifikatsiyu yazyk C-light // Sistemnaya informatika: sbornik nauchnykh trudov. Novosibirsk: Izdatelstvo SO RAN, 2004. Vyp. 9: Formalnye metody i modeli informatiki. P. 51 – 134 [in Russian]).Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. Ориентированный на верификацию язык C-light // Системная информатика: сборник научных трудов. Новосибирск: Издательство СО РАН. 2004. Вып. 9: Формальные методы и модели информатики. С. 51 – 134 (Nepomnyaschy V.A., Anureev I.S., Mikhaylov I.N., Promsky A.V. Orientirovanny na verifikatsiyu yazyk C-light // Sistemnaya informatika: sbornik nauchnykh trudov. Novosibirsk: Izdatelstvo SO RAN, 2004. Vyp. 9: Formalnye metody i modeli informatiki. P. 51 – 134 [in Russian]).Anureev I.S., Maryasov I.V., Nepomniaschy V.A. C-programs Verification Based on Mixed Axiomatic Semantics // Automatic Control and Computer Sciences. 2011. Vol. 45. Issue 7. P. 485–500.Anureev I.S., Maryasov I.V., Nepomniaschy V.A. C-programs Verification Based on Mixed Axiomatic Semantics // Automatic Control and Computer Sciences. 2011. Vol. 45. Issue 7. P. 485–500.Anureev I., Maryasov I., Nepomniaschy V. Revised Mixed Axiomatic Semantics Method of C Program Verification // Proc. of 3rd Workshop "PSSV: Theory and Applications". Nizhni Novgorod, 2012. P. 16–23.Anureev I., Maryasov I., Nepomniaschy V. Revised Mixed Axiomatic Semantics Method of C Program Verification // Proc. of 3rd Workshop "PSSV: Theory and Applications". Nizhni Novgorod, 2012. P. 16–23.Baudin P., Cuoq P., Filliˆatre J.-C., March´e C., Monate B., Moy Y., Prevosto V. ACSL: ANSI/ISO C Specification Language. http://frama-c.com/download/acsl_1.4.pdfBaudin P., Cuoq P., Filliˆatre J.-C., March´e C., Monate B., Moy Y., Prevosto V. ACSL: ANSI/ISO C Specification Language. http://frama-c.com/download/acsl_1.4.pdfBormer T., Brockschmidt M., Distefano D., Ernst G., Filliˆatre J.-C., Grigore R., Huisman M., Klebanov V., March´e C., Monahan R., Mostowski W., Polikarpova N., Scheben C., Schellhorn G., Tofan B., Tschannen J., Ulbrich M. The COST IC0701 Verification Competition 2011 // Revised Selected Papers of Int. Conf. FoVeOOS 2011. LNCS. 2011. Vol.7421. P. 3–21.Bormer T., Brockschmidt M., Distefano D., Ernst G., Filliˆatre J.-C., Grigore R., Huisman M., Klebanov V., March´e C., Monahan R., Mostowski W., Polikarpova N., Scheben C., Schellhorn G., Tofan B., Tschannen J., Ulbrich M. The COST IC0701 Verification Competition 2011 // Revised Selected Papers of Int. Conf. FoVeOOS 2011. LNCS. 2011. Vol.7421. P. 3–21.Cohen E., Dahlweid M., Hillebrand M., Leinenbach D., Moskal M., Santen T., Schulte W., Tobies S. VCC: A Practical System for Verifying Concurrent C // Proc. of 22nd Int. Conf. TPHOLs. LNCS. 2009. Vol. 5674. P. 23–42.Cohen E., Dahlweid M., Hillebrand M., Leinenbach D., Moskal M., Santen T., Schulte W., Tobies S. VCC: A Practical System for Verifying Concurrent C // Proc. of 22nd Int. Conf. TPHOLs. LNCS. 2009. Vol. 5674. P. 23–42.Detlefs D., Nelson G., Saxe J. B. Simplify: A Theorem Prover for Program Checking. Palo Alto, 2003. 121 p. (HP Tech. Rep. HPL-2003-148). http://www.hpl.hp.com/techreports/2003/HPL-2003-148.pdfDetlefs D., Nelson G., Saxe J. B. Simplify: A Theorem Prover for Program Checking. Palo Alto, 2003. 121 p. (HP Tech. Rep. HPL-2003-148). http://www.hpl.hp.com/techreports/2003/HPL-2003-148.pdfFilliˆatre J.-C., March´e C. Multi-prover Verification of C Programs // Proc. of 6th ICFEM. LNCS. 2004. Vol. 3308. P. 15–29.Filliˆatre J.-C., March´e C. Multi-prover Verification of C Programs // Proc. of 6th ICFEM. LNCS. 2004. Vol. 3308. P. 15–29.Klebanov V., M¨uller P., Shankar N., Leavens G. T., W¨ustholz V., Alkassar E., Arthan R., Bronish D., Chapman R., Cohen E., Hillebrand M., Jacobs B., Leino K. R. M., Monahan R., Piessens F., Polikarpova N., Ridge T., Smans J., Tobies S., Tuerk T., Ulbrich M., Weiß B. The 1st Verified Software Competition: Experience Report // Proc. 17th Int. Symp. on Formal Methods. LNCS. 2011. Vol. 6664. P. 154–168.Klebanov V., M¨uller P., Shankar N., Leavens G. T., W¨ustholz V., Alkassar E., Arthan R., Bronish D., Chapman R., Cohen E., Hillebrand M., Jacobs B., Leino K. R. M., Monahan R., Piessens F., Polikarpova N., Ridge T., Smans J., Tobies S., Tuerk T., Ulbrich M., Weiß B. The 1st Verified Software Competition: Experience Report // Proc. 17th Int. Symp. on Formal Methods. LNCS. 2011. Vol. 6664. P. 154–168.Leino K.R.M. Dafny: An Automatic Program Verifier for Functional Correctness // Revised Selected Papers of 16th Int. Conf. LPAR-16. LNCS. 2010. Vol. 6355. P. 348–370.Leino K.R.M. Dafny: An Automatic Program Verifier for Functional Correctness // Revised Selected Papers of 16th Int. Conf. LPAR-16. LNCS. 2010. Vol. 6355. P. 348–370.Maryasov I.V., Nepomniaschy V.A., Promsky A.V., Kondratyev D.A. Automatic C Program Verification Based on Mixed Axiomatic Semantics // Proc. of 4th Workshop "PSSV: Theory and Applications". Yekaterinburg, 2013. P. 50–59.Maryasov I.V., Nepomniaschy V.A., Promsky A.V., Kondratyev D.A. Automatic C Program Verification Based on Mixed Axiomatic Semantics // Proc. of 4th Workshop "PSSV: Theory and Applications". Yekaterinburg, 2013. P. 50–59.Moura L. de, Bjørner N. Z3: An Efficient SMT Solver // Proc. of 14th Int. Conf. TACAS 2008. LNCS. 2008. Vol. 4963. P. 337–340.Moura L. de, Bjørner N. Z3: An Efficient SMT Solver // Proc. of 14th Int. Conf. TACAS 2008. LNCS. 2008. Vol. 4963. P. 337–340.Nepomniaschy V.A., Anureev I.S., Atuchin M.M., Maryasov I.V., Petrov A.A., Promsky A.V. C Program Verification in SPECTRUM Multilanguage System // Automatic Control and Computer Sciences. 2011. Vol. 45. Issue 7. P. 413–420.Nepomniaschy V.A., Anureev I.S., Atuchin M.M., Maryasov I.V., Petrov A.A., Promsky A.V. C Program Verification in SPECTRUM Multilanguage System // Automatic Control and Computer Sciences. 2011. Vol. 45. Issue 7. P. 413–420.Promsky A.V. A Formal Approach To The Error Localization. Novosibirsk, 2012. 33 p. (Preprint / RAS. Sib. branch. IIS; No 169).Promsky A.V. A Formal Approach To The Error Localization. Novosibirsk, 2012. 33 p. (Preprint / RAS. Sib. branch. IIS; No 169).

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