Метод моделирования памяти в предикатных абстракциях с разделением на непересекающиеся области
https://doi.org/10.15514/ISPRAS-2017-29(4)-13
Аннотация
Верификация программного обеспечения - вид деятельности, направленный на контроль качества программного обеспечения и обнаружения ошибок в нем. Статическая верификация - это один из способов верификации, который производится без выполнения исходного кода программы. Для статической верификации используется специальное программное обеспечение: инструменты статической верификации, которые часто работают с исходным кодом программы. Одним из таких инструментов является инструмент под названием CPAchecker. Проблема его текущей модели памяти заключается в том, что при встрече функции, возвращающей указатель на область памяти, у которой отсутствует тело, в процессе верификации о ее возвращаемом значении могут быть сделаны произвольные предположения. Несмотря на то, что они теоретически допустимы, вероятность их выполнения на практике очень низка. Использование этих предположений может привести к ложному предупреждению в качестве результата верификации. В данной статье мы делаем обзор на один из подходов, благодаря которому можно избавиться от такой проблемы, а также предлагаем формальное описание данного подхода в терминах формул путей, содержащих неинтерпретируемые функции, которые инструмент использует для моделирования памяти программы. Также мы приводим результаты сравнительного анализа эффективности предложенной реализации относительно существующей модели памяти.
Об авторах
А. Р. Волков
Московский государственный университет имени М.В. Ломоносова
Россия
Россия
М. У. Мандрыкин
Институт системного программирования РАН
Россия
Россия
Список литературы
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
Послать статью по эл. почте 