Автоматическое доказательство корректности программ с динамической памятью
Юрий Олегович Костюков,
Константин Аланович Батоев,
Дмитрий Александрович Мордвинов,
Михаил Павлович Костицын,
Александр Владимирович Мисонижник https://doi.org/10.15514/ISPRAS-2019-31(5)-3
Аннотация
В данной работе изучаются теоретические основы автоматической модульной верификации императивных программ с динамической памятью. Вводится формализм композициональной символьной памяти, который используется для построения композиционального алгоритма, порождающего обобщённые кучи. Они являются термами исчисления символьных куч, которые описывают состояния произвольных циклических фрагментов программы. Выводимые в этом исчислении кучи соответствуют достижимым состояниям исходной программы. В работе также устанавливается соответствие между выводом в этом исчислении и исполнением функциональных программ второго порядка без эффектов.
Об авторах
Юрий Олегович Костюков
Санкт-Петербургский государственный университет
Россия
Получил степень бакалавра в области информационных технологий в Санкт-Петербургском государственном университете в 2019 г.
Россия
Получил степень бакалавра в области информационных технологий в Санкт-Петербургском государственном университете в 2019 г.
Константин Аланович Батоев
Санкт-Петербургский государственный университет
Россия
Получил степень бакалавра в области информационных технологий в Санкт-Петербургском государственном университете в 2019 г.
Россия
Получил степень бакалавра в области информационных технологий в Санкт-Петербургском государственном университете в 2019 г.
Дмитрий Александрович Мордвинов
Санкт-Петербургский государственный университет,
JetBrains Research
Россия
Старший преподаватель, готовит диссертацию на соискание степени PhD в области информационных технологий
Россия
Старший преподаватель, готовит диссертацию на соискание степени PhD в области информационных технологий
Михаил Павлович Костицын
Санкт-Петербургский государственный университет
Россия
Получил степень бакалавра в области информационных технологий в Санкт-Петербургском государственном университете в 2019 г.
Россия
Получил степень бакалавра в области информационных технологий в Санкт-Петербургском государственном университете в 2019 г.
Александр Владимирович Мисонижник
Санкт-Петербургский государственный университет
Россия
Получил степень бакалавра в области информационных технологий в Санкт-Петербургском государственном университете в 2018 г.
Россия
Получил степень бакалавра в области информационных технологий в Санкт-Петербургском государственном университете в 2018 г.
Список литературы
1. Distefano D. Attacking large industrial code with bi-abductive inference. Lecture Notes in Computer Science, vol. 5825, 2009, pp. 1–8.
2. Calcagno C. et al. Compositional shape analysis by means of bi-abduction. Journal of the ACM, vol. 58, no. 6, 2011, p. 26:1-26:66.
3. Gurfinkel A. et al. The SeaHorn verification framework. Lecture Notes in Computer Science, vol. 9206, 2015, pp. 343–361.
4. Anand S., Godefroid P., and Tillmann N. Demand-driven compositional symbolic execution. Lecture Notes in Computer Science, vol. 4963, 2008, pp. 367–381.
5. Distefano D. and Parkinson J M. J. jStar: Towards practical verification for Java. ACM Sigplan Notices, vol. 43, issue 10, 2008, pp. 213– 226.
6. Calcagno C. and Distefano D. Infer: An automatic program verifier for memory safety of C programs. Lecture Notes in Computer Science, vol. 6617, 2011, pp. 459–465.
7. Tillmann N. and De Halleux J. Pex–white box test generation for. net. Lecture Notes in Computer Science, vol. 4966, 2008, pp. 134– 153.
8. Cousot P. and Cousot R. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, 1977, pp. 238– 252.
9. Khurshid S., Păsăreanu C. S., and Visser W. Generalized Symbolic Execution for Model Checking and Testing. Lecture Notes in Computer Science, vol. 2619, 2003, pp. 553–568.
10. Vazou N., Bakst A., and Jhala R. Bounded refinement types. ACM SIGPLAN Notices, vol. 50, issue 9, 2015, pp. 48–61.
11. Godefroid P. Compositional Dynamic Test Generation. ACM SIGPLAN Notices, vol. 42, issue 1, 2007, pp. 47–54.
12. Biere A. et al. Symbolic Model Checking without BDDs. Lecture Notes in Computer Science, vol. 1579, 1999, pp. 193–207.
13. Deng X., Lee J. et al. Efficient and Formal Generalized Symbolic Execution. Automated Software Engineering, vol. 19, issue 3, 2012, pp. 233–301.
14. Braione P., Denaro G., and Pezz`e M. JBSE: A symbolic executor for java programs with complex heap inputs. In Proc. of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2016, pp. 1018–1022.
15. Reynolds J. C. Separation logic: A logic for shared mutable data structures. In Proc. 17th Annual IEEE Symposium on Logic in Computer Science, 2002, pp. 55–74.
16. Sagiv M., Reps T., and Wilhelm R. Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems, vol. 24, issue 3. 2002, pp. 217–298.
17. Berdine J., Calcagno C., and O’Hearn P.W. Symbolic execution with separation logic. Lecture Notes in Computer Science, vol. 3780, 2005, pp. 52–68.
18. Dudka K., Peringer P., and Vojnar T. Byte-precise verification of lowlevel list manipulation. Lecture Notes in Computer Science, vol. 7935, 2013, pp. 215–237.
19. Barrett C. and Tinelli C. Satisfiability modulo theories. In Handbook of Model Checking, Springer, 2018, pp. 305–343.
20. Kahsai T. et al. Quantified heap invariants for object-oriented programs. In Proc. of the 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2017, pp. 368– 384.
21. Torlak E. and Bodik R. A lightweight symbolic virtual machine for solver-aided host languages. ACM SIGPLAN Notices, vol. 49, issue 6, 2014, pp. 530–541.
22. Baldoni R. et al. A survey of symbolic execution techniques. ACM Computing Surveys, vol. 51, no. 3, 2018, pp. 50:1-50:39.
23. Unno H., Terauchi T., and Kobayashi N. Automating relatively complete verification of higher-order functional programs. ACM SIGPLAN Notices, vol. 48, issue 1, 2013, pp. 75 86.
24. Zhu H. and Jagannathan S. Compositional and lightweight dependent type inference for ML. Lecture Notes in Computer Science, vol. 7737, 2013, pp. 295–314.
25. Cathcart Burn T., Ong C.-H.L., and Ramsay S. J. Higher-order constrained horn clauses for verification. Proceedings of the ACM on Programming Languages vol. 2, no. POPL, 2017, p. 11:1-11:27.
26. Мандрыкин М.У., Мутилин В.С.. Обзор подходов к моделированию памяти в инструментах статической верификации. Труды ИСПРАН, том 29, вып. 1, 2017 г., стр. 195-230 / Mandrykin M.U., Mutilin V.S. Survey of memory modeling methods in static verification tools. Trudy ISP RAN / Proc. ISP RAS, vol. 29, issue 1, 2017, pp. 195-230 (in Russian). DOI: 10.15514/ISPRAS-2017-29(1)-12.
27. Костюков Ю. О., Батоев К. А., Мордвинов Д. А., Костицын М. П., Мисонижник А. В. Автоматическое доказательство корректности программ с динамической памятью. arXiv:1906.10204, 2019 г. / Kostyukov Yu.O., Batoev K.A., Mordvinov D.A., Kostitsyn M.P., Misonizhnik A.V.. Automatic verification of heap-manipulating programs. arXiv:1906.10204, 2019 (in Russian).
28. Терехов А.Н. Технология программирование встроенных систем. автореферат дис. доктора физико-математических наук. Новосибирск, 1991 г. / Terekhov A.N. Technology for programming of embedded systems. Abstract of Thesis for obtaining the degree of Doctor of physical and mathematical sciences. Novosibirsk, 1991 (in Russian).
29. Новиков Е.М. Развитие ядра операционной системы Linux. Труды ИСП РАН, том 29, вып. 2, 2017 г., стр. 77-96 / Novikov E.M. Evolution of the Linux kernel. Trudy ISP RAN/Proc. ISP RAS, vol. 29, issue 2, 2017, pp. 77-96 (in Russian). DOI: 10.15514/ISPRAS-2017-29(2)-3.
30. Ольхович Л.Б., Кознов Д.В. Метод автоматической валидации UML-спецификаций на языке OCL. Программирование, том 29. № 6, 2003 г., стр. 44-50 / Ol'khovich L., Koznov D.V. OCL-based automated validation method for UML specifications. Programming and Computer Software, vol. 29, № 6, 2003, pp. 323-327.
Рецензия
Для цитирования:
Костюков Ю.О., Батоев К.А., Мордвинов Д.А., Костицын М.П., Мисонижник А.В. Автоматическое доказательство корректности программ с динамической памятью. Труды Института системного программирования РАН. 2019;31(5):37-62. https://doi.org/10.15514/ISPRAS-2019-31(5)-3
For citation:
Kostyukov Yu., Batoev K., Mordvinov D., Kostitsyn M., Misonizhnik A. Automatic verification of heap-manipulating programs. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2019;31(5):37-62. (In Russ.) https://doi.org/10.15514/ISPRAS-2019-31(5)-3
Послать статью по эл. почте 