References

mais

Моделирование и анализ информационных систем

Modeling and Analysis of Information Systems

1818-10152313-5417

Yaroslavl State University

10.18255/1818-1015-2021-4-372-393

mais-1566

Research Article

Theory of Computing

На пути к автоматической дедуктивной верификации C-программ с Sisal-циклами в системе C-lightVer

Towards Automatic Deductive Verification of C Programs with Sisal Loops Using the C-lightVer System

https://orcid.org/0000-0002-9387-6735

Кондратьев

Дмитрий Александрович

Kondratyev

Dmitry A.

apple-66@mail.ru

Институт систем информатики им. А.П. ЕршоваРоссияA.P. Ershov Institute of Informatics SystemsRussian Federation

2021

18122021

284372393

2021

Кондратьев Д.А.

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/1566

В Институте систем информатики СО РАН разрабатывается система C-lightVer для дедуктивной верификации C-программ. C-kernel является промежуточным языком верификации в данной системе. Система облачного параллельного программирования (CPPS) также разрабатывается в Институте систем информатики СО РАН. Cloud Sisal является входным языком системы CPPS. Главной особенностью системы CPPS является неявное параллельное исполнение, основанное на автоматическом распараллеливании циклов Cloud Sisal. Cloud-Sisal-kernel является промежуточным языком верификации в системе CPPS. Нашей целью является автоматическое распараллеливание такого надмножества языка C, которое позволяет реализовать автоматическую верификацию. Нашим решением является такое надмножество языка C-kernel, как язык C-Sisal-kernel. Первым результатом, представленным в данной статье, является расширение языка C-kernel циклами языка Cloud-Sisal-kernel. В результате был разработан язык C-Sisal-kernel. Вторым результатом, представленным в данной статье, является расширение аксиоматической семантики языка C-kernel правилом вывода для циклов языка Cloud-Sisal-kernel. В данной статье также представлен наш подход к проблеме автоматизации дедуктивной верификации в случае финитных итераций над структурами данных. Такие циклы называются финитными итерациями. Нашим решением является композиция символического метода верификации финитных итераций, метагенерации условий корректности и смешанной аксиоматической семантики. Символический метод верификации финитных итераций позволяет задавать правила вывода для таких циклов без инвариантов. Символическая замена финитных итераций рекурсивными функциями является основой данного метода. Полученные условия корректности с применениями рекурсивных функций соответствуют логической основе системы доказательства ACL2. Мы используем систему ACL2, основанную на вычислимых рекурсивных функциях. Метагенерация условий корректности позволяет упростить реализацию новых правил вывода в системе верификации. Использование смешанной аксиоматической семантики приводит в некоторых случаях к более простым условиям корректности.

The C-lightVer system is developed in IIS SB RAS for C-program deductive verification. C-kernel is an intermediate verification language in this system. Cloud parallel programming system (CPPS) is also developed in IIS SB RAS. Cloud Sisal is an input language of CPPS. The main feature of CPPS is implicit parallel execution based on automatic parallelization of Cloud Sisal loops. Cloud-Sisal-kernel is an intermediate verification language in the CPPS system. Our goal is automatic parallelization of such a superset of C that allows implementing automatic verification. Our solution is such a superset of C-kernel as C-Sisal-kernel. The first result presented in this paper is an extension of C-kernel by Cloud-Sisal-kernel loops. We have obtained the C-Sisal-kernel language. The second result is an extension of C-kernel axiomatic semantics by inference rule for Cloud-Sisal-kernel loops. The paper also presents our approach to the problem of deductive verification automation in the case of finite iterations over data structures. This kind of loops is referred to as definite iterations. Our solution is a composition of symbolic method of verification of definite iterations, verification condition metageneration and mixed axiomatic semantics method. Symbolic method of verification of definite iterations allows defining inference rules for these loops without invariants. Symbolic replacement of definite iterations by recursive functions is the base of this method. Obtained verification conditions with applications of recursive functions correspond to logical base of ACL2 prover. We use ACL2 system based on computable recursive functions. Verification condition metageneration allows simplifying implementation of new inference rules in a verification system. The use of mixed axiomatic semantics results to simpler verification conditions in some cases.

дедуктивная верификацияC-lightVerсистема облачного параллельного программированиясимволический метод верификации финитных итерацийинвариант циклаACL2

deductive verificationC-lightVercloud parallel programming systemsymbolic method of verification of definite iterationsloop invariantACL2

References1

I. V. Maryasov, V. A. Nepomniaschy, A. V. Promsky, and D. A. Kondratyev, “Automatic C Program Verification Based on Mixed Axiomatic Semantics,” Automatic Control and Computer Sciences, vol. 48, no. 7, pp. 407-414, 2014.

D. A. Kondratyev and A. V. Promsky, “Developing a self-applicable verification system. Theory and practice,” Automatic Control and Computer Sciences, vol. 49, no. 7, pp. 445-452, 2015.

D. Kondratyev, “Implementing the Symbolic Method of Verification in the C-Light Project,” in Perspectives of System Informatics, vol. 10742, Springer, 2018, pp. 227-240.

D. A. Kondratyev, I. V. Maryasov, and V. A. Nepomniaschy, “The Automation of C Program Verification by the Symbolic Method of Loop Invariant Elimination,” Automatic Control and Computer Sciences, vol. 53, no. 7, pp. 653-662, 2019.

D. A. Kondratyev and A. V. Promsky, “The Complex Approach of the C-lightVer System to the Automated Error Localization in C-Programs,” Automatic Control and Computer Sciences, vol. 54, no. 7, pp. 728-739, 2020.

C. A. R. Hoare, “An axiomatic basis for computer programming,” Communications of the ACM, vol. 12, no. 10, pp. 576-580, 1969.

K. R. Apt and E.-R. Olderog, “Fifty years of Hoare’s logic,” Formal Aspects of Computing, vol. 31, no. 6, pp. 751-807, 2019.

R. H\"ahnle and M. Huisman, “Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools,” in Computing and Software Science, vol. 10000, Springer, 2019, pp. 345-373.

K. R. Apt and E.-R. Olderog, “Assessing the Success and Impact of Hoare’s Logic,” in Theories of Programming: The Life and Works of Tony Hoare, 2021, pp. 41-76.

V. A. Nepomniaschy, I. S. Anureev, I. N. Mikhailov, and A. V. Promskii, “Towards verification of C programs. C-light language and its formal semantics,” Programming and Computer Software, vol. 28, no. 6, pp. 314-323, 2002.

V. A. Nepomniaschy, I. S. Anureev, and A. V. Promskii, “Towards Verification of C Programs: Axiomatic Semantics of the C-kernel Language,” Programming and Computer Software, vol. 29, no. 6, pp. 338-350, 2003.

V. A. Nepomniaschy, “Symbolic method of verification of definite iterations over altered data structures,” Programming and Computer Software, vol. 31, no. 1, pp. 1-9, 2005.

M. Moriconi and R. L. Schwartz, “Automatic construction of verification condition generators from hoare logics,” in International Colloquium on Automata, Languages, and Programming, vol. 115, Springer, 1981, pp. 363-377.

J. S. Moore, “Milestones from the Pure Lisp Theorem Prover to ACL2,” Formal Aspects of Computing, vol. 31, no. 6, pp. 699-732, 2019.

V. Kasyanov and E. Kasyanova, “Methods and System for Cloud Parallel Programming,” in Proceedings of the 21st International Conference on Enterprise Information Systems, 2019, vol. 1, pp. 623-629.

V. N. Kasyanov and A. P. Stasenko, “Sisal 3.2 Language Structure Decomposition,” in Proceedings of the European Computing Conference, vol. 28, Springer, 2009, pp. 533-543.

A. Stasenko, “Sisal 3.2 Language Features Overview,” in International Conference on Parallel Computing Technologies, vol. 6873, Springer, 2011, pp. 110-124.

V. Kasyanov, “Sisal 3.2: functional language for scientific parallel programming,” Enterprise Information Systems, vol. 7, no. 2, pp. 227-236, 2013.

J. T. Feo, D. C. Cann, and R. R. Oldehoeft, “A report on the sisal language project,” Journal of Parallel and Distributed Computing, vol. 10, no. 4, pp. 349-366, 1990.

J.-L. Gaudiot, T. DeBoni, J. Feo, W. B\"ohm, W. Najjar, and P. Miller, “The Sisal Project: Real World Functional Programming,” in Compiler Optimizations for Scalable Parallel Systems, vol. 1808, Springer, 2001, pp. 45-72.

K. Pyzhov and R. Idrisov, “Back-end translator for Sisal 3.1 compiler,” Bulletin of the Novosibirsk Computing Center, no. 35, pp. 101-119, 2013.

D. A. Kondratyev and A. V. Promsky, “Towards verification of scientific and engineering programs. The CPPS project,” Journal of Computational Technologies, vol. 25, no. 5, pp. 91-106, 2020.

J. Dean and S. Ghemawat, “MapReduce: simplified data processing on large clusters,” in Proceedings of the 6th conference on Symposium on Operating Systems Design & Implementation, 2004, vol. 6.

M. Kaufmann and J. S. Moore, “Iteration in ACL2,” in Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications, vol. 327, 2020, pp. 16-31.

S. Blom, S. Darabi, M. Huisman, and M. Safari, “Correct program parallelisations,” International Journal on Software Tools for Technology Transfer, vol. 23, no. 5, pp. 741-763, 2021.

B. Jacobs, J. Kiniry, and M. Warnier, “Java Program Verification Challenges,” in Formal Methods for Components and Objects, vol. 2852, Springer, 2003, pp. 202-219.

D. R. Cok, “Reasoning about Functional Programming in Java and C++,” in Companion Proceedings for the ISSTA/ECOOP 2018 Workshops, 2018, pp. 37-39.

D. R. Cok and S. Tasiran, “Practical Methods for Reasoning About Java 8's Functional Programming Features,” in Verified Software: Theories, Tools, and Experiments, vol. 11294, Springer, 2018, pp. 267-278.

ISO/IEC 14882:2020: Programming language C++. ISO/IEC, 2020.

ISO/IEC 9899:2011: Programming language C. ISO/IEC, 2011.

R. Krebbers and F. Wiedijk, “A Typed C11 Semantics for Interactive Theorem Proving,” in Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015, pp. 15-27.

M. Sammler, R. Lepigre, R. Krebbers, K. Memarian, D. Dreyer, and D. Garg, “RefinedC: automating the foundational verification of C code with refined ownership types,” in Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021, pp. 158-174.

M. O. Myreen and M. J. C. Gordon, “Transforming Programs into Recursive Functions,” Electronic Notes in Theoretical Computer Science, vol. 240, pp. 185-200, 2009.

R. Blanc, V. Kuncak, E. Kneuss, and P. Suter, “An overview of the Leon verification system: verification by translation to recursive functions,” in Proceedings of the 4th Workshop on Scala, 2013, pp. 1-10.

A. Humenberger, M. Jaroschek, and L. Kov\'acs, “Invariant Generation for Multi-Path Loops with Polynomial Assignments,” in Verification, Model Checking, and Abstract Interpretation, vol. 10747, Springer, 2018, pp. 226-246.

S. Chakraborty, A. Gupta, and D. Unadkat, “Diffy: Inductive Reasoning of Array Programs Using Difference Invariants,” in Computer Aided Verification, vol. 12760, Springer, 2021, pp. 911-935.

T. Tuerk, “Local reasoning about while-loops,” in Proceedings of the Theory Workshop at VSTTE 2010, 2010, pp. 29-39.

A. Blanchard, F. Loulergue, and N. Kosmatov, “Towards Full Proof Automation in Frama-C Using Auto-active Verification,” in NASA Formal Methods, vol. 11460, Springer, 2019, pp. 88-105.

P. Baudin et al., “The dogged pursuit of bug-free C programs: the Frama-C software analysis platform,” Communications of the ACM, vol. 64, no. 8, pp. 56-68, 2021.

I. Attali, D. Caromel, and A. Wendelborn, “A Formal Semantics and an Interactive Environment for Sisal,” in Tools and Environments for Parallel and Distributed Systems, vol. 2, Springer, 1996, pp. 229-256.

D. Kondratyev and A. Promsky, “Proof Strategy for Automated Sisal Program Verification,” in Software Technology: Methods and Tools, vol. 11771, Springer, 2019, pp. 113-120.

B. Beckert, T. Bingmann, M. Kiefer, P. Sanders, M. Ulbrich, and A. Weigl, “Relational Equivalence Proofs Between Imperative and MapReduce Algorithms,” in Verified Software. Theories, Tools, and Experiments, vol. 11294, Springer, 2018, pp. 248-266.

G. Parthasarathy, P. M\"uller, and A. J. Summers, “Formally Validating a Practical Verification Condition Generator,” in Computer Aided Verification, vol. 12760, Springer, 2021, pp. 704-727.

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