Preview

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

Расширенный поиск

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

https://doi.org/10.18255/1818-1015-2021-4-372-393

Полный текст:

Аннотация

В Институте систем информатики СО РАН разрабатывается система 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, основанную на вычислимых рекурсивных функциях. Метагенерация условий корректности позволяет упростить реализацию новых правил вывода в системе верификации. Использование смешанной аксиоматической семантики приводит в некоторых случаях к более простым условиям корректности.

Об авторе

Дмитрий Александрович Кондратьев
Институт систем информатики им. А.П. Ершова
Россия


Список литературы

1. 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.

2. 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.

3. 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.

4. 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.

5. 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.

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

7. 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.

8. 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.

9. 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.

10. 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.

11. 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.

12. 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.

13. 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.

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

15. 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.

16. 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.

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

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

19. 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.

20. 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.

21. 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.

22. 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.

23. 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.

24. 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.

25. 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.

26. 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.

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

28. 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.

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

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

31. 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.

32. 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.

33. 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.

34. 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.

35. 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.

36. 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.

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

38. 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.

39. 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.

40. 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.

41. 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.

42. 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.

43. 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.


Рецензия

Для цитирования:


Кондратьев Д.А. На пути к автоматической дедуктивной верификации C-программ с Sisal-циклами в системе C-lightVer. Моделирование и анализ информационных систем. 2021;28(4):372-393. https://doi.org/10.18255/1818-1015-2021-4-372-393

For citation:


Kondratyev D.A. Towards Automatic Deductive Verification of C Programs with Sisal Loops Using the C-lightVer System. Modeling and Analysis of Information Systems. 2021;28(4):372-393. (In Russ.) https://doi.org/10.18255/1818-1015-2021-4-372-393

Просмотров: 86


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)