Моделирование памяти Си-программ для инструментов статической верификации на основе SMT-решателей

Авторы

М.У. Мандрыкин

Аннотация

Цель работы — разработка и реализация методов моделирования памяти Си-программ, адаптированных для модулей ядра ОС Linux, для применения в инструментах автоматической статической и дедуктивной верификации, использующих SMT-решатели. Теоретическая и практическая значимость В работе предложено две модели памяти для использования в инструментах автоматической статической и дедуктивной верификации Си-программ.

Полный текст статьи в формате pdf

Издание

Диссертация на соискание ученой степени к.ф-м.н., Москва, 2016 г.

Научная группа

Технологии программирования

Все публикации за 2013 год

Все публикации