Войти / Регистрация
Корзина

  • Ваша корзина пуста
Войти / Регистрация
Корзина

  • Ваша корзина пуста

Статья «АНАЛИЗ РЕГИОНОВ ДЛЯ ДЕДУКТИВНОЙ ВЕРИФИКАЦИИ Си-ПРОГРАММ, "Программирование"»

Авторы:
  • Мандрыкин М.У.1
  • Хорошилов А.В.2
стр. 3-29
Платно
1 Институт системного программирования РАН, 2 Институт системного программирования РАН; Московский физико-технический институт (государственный университет)
  • В выпуске: №5, 2016
  • В журнале: Программирование
  • Издательство: ФГУП «Издательство «Наука»
  • Рубрика ГРНТИ: Информатика. Информационные и вычислительные системы
  • Год выхода: 2016
  • SDI: 007.001.0132-3474.2016.000.005.3.29
  • ISSN: 0132-3474
  • УДК: 004.45
Аннотация:
В статье предложена модель памяти с разделением на непересекающнеся области (регионы), предназначенная для дедуктивной верификации Си-программ. Модель памяти опирается на использование базового языка с поддержкой произвольной вложенности структур, объединений и массивов в другие структуры, а также соответствующего анализа регионов, уменьшающего число необходимых задаваемых пользователем аннотаций. В статье определена семантика базового языка, описаны нормализующие преобразования, позволяющие преобразовать исходную аннотированную Си-программу в соответствующую программу на базовом языке. Предложен способ представления состояния памяти программ на базовом языке в виде логических формул, представленный в виде модельной семантики базового языка. Для модельной семантики приведены доказательства теорем о корректности и полноте. Описаны дополнительные ограничения на контекст типизации термов базового языка, которые определяют результат анализа регионов, позволяющего полно моделировать ограниченный класс программ без использования дополнительных аннотаций. Приведен план доказательства теоремы о полноте предложенного анализа регионов для ограниченного класса программ.

Архивные статьи (2015 год и ранее) доступны для ознакомления бесплатно, для скачивания их необходимо приобрести. Для просмотра материалов необходимо зарегистрироваться и авторизоваться на сайте.

Чтобы приобрести доступ к материалу для юридического лица, пожалуйста, свяжитесь с администрацией портала с помощью формы обратной связи либо по электронному адресу libnauka@naukaran.com.  

Действия с материалами доступны только авторизованным пользователям.