Метод моделирования памяти в предикатных абстракциях с разделением на непересекающиеся области
https://doi.org/10.15514/ISPRAS-2017-29(4)-13
Аннотация
Об авторах
А. Р. Волков
Московский государственный университет имени М.В. Ломоносова
Россия
Россия
М. У. Мандрыкин
Институт системного программирования РАН
Россия
Россия
Список литературы
1. В.В. Кулямин, “Методы верификации программного обеспечения” Всероссийский конкурсный отбор обзорно-аналитических статей по приоритетному направлению "Информационно-телекоммуникационные системы", 117 стр., 2008.
2. D. Beyer, T. A. Henzinger, and G. Theoduloz, “Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis,” in Computer Aided Verification, ser. Lecture Notes in Computer Science, W. Damm and H. Hermanns, Eds., vol. 4590. Berlin, Heidelberg: Springer Berlin Heidelberg, 2006, pp. 504-518.
3. M. Mandrykin and A. Khoroshilov, “A memory model for deductively verifying Linux kernel modules,” A.P. Ershov Informatics Conference, the PSI Conference Series, 11th edition, 2017 (to appear).
4. Мандрыкин М.У. и Мутилин В.С., “Моделирование памяти с использованием неинтерпретируемых функций в предикатных абстракциях” Труды ИСП РАН, том 27, вып. 5, 2015, стр. 117-142. DOI: 10.15514/ISPRAS-2015-27(5)-7
5. R. Bornat, “Proving pointer programs in Hoare Logic,” in Mathematics of Program Construction: 5th International Conference, MPC 2000, ser. Lecture Notes in Computer Science, R. Backhouse and J. N. Oliveira, Eds., vol. 1837. Berlin, Heidelberg: Springer Berlin Heidelberg, 2000, pp. 102-126.
6. R. Burstall, “Some techniques for proving correctness of programs which alter data structures,” Machine Intelligence, vol. 7, pp. 23-50, 1972.
Рецензия
Для цитирования:
Волков А.Р., Мандрыкин М.У. Метод моделирования памяти в предикатных абстракциях с разделением на непересекающиеся области. Труды Института системного программирования РАН. 2017;29(4):203-216. https://doi.org/10.15514/ISPRAS-2017-29(4)-13
For citation:
Volkov A.R., Mandrykin M.U. Predicate Abstractions Memory Modeling Method with Separation into Disjoint Regions. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2017;29(4):203-216. https://doi.org/10.15514/ISPRAS-2017-29(4)-13
Послать статью по эл. почте 