РОССИЙСКАЯ ФЕДЕРАЦИЯ
ФЕДЕРАЛЬНАЯ СЛУЖБА ПО ИНТЕЛЛЕКТУАЛЬНОЙ СОБСТВЕННОСТИ
ГОСУДАРСТВЕННАЯ РЕГИСТРАЦИЯ ПРОГРАММЫ ДЛЯ ЭВМ

Номер регистрации (свидетельства): 2016618347

Дата регистрации: 27.07.2016

Номер и дата поступления заявки: 2016616275 14.06.2016

Дата публикации: 20.08.2016
	
Авторы:
Мандрыкин Михаил Усамович,
Хорошилов Алексей Владимирович

Правообладатель:
ФЕДЕРАЛЬНОЕ ГОСУДАРСТВЕННОЕ БЮДЖЕТНОЕ УЧРЕЖДЕНИЕ НАУКИ ИНСТИТУТ СИСТЕМНОГО ПРОГРАММИРОВАНИЯ РОССИЙСКОЙ АКАДЕМИИ НАУК

Название программы для ЭВМ:
Программа дедуктивной верификации программ на языке Си, использующая модель памяти с чувствительным к контексту разделением на непересекающиеся регионы

Реферат:
Данное программное обеспечение используется для дедуктивной верификации программ на языке Си, аннотированных спецификациями на языке ACSL, с помощью трансляции через промежуточный язык Jessie в Why3ML - входной язык платформы статической верификации Why3, генерирующей соответствующие заданным спецификациям условия верификации. Основной особенностью данной программы является использование модели памяти с разделением на непересекающиеся регионы, которая упрощает доказательство условий верификации для базовых путей, на которых происходит большое число обновлений памяти по не совпадающим адресам, и поддерживает произвольную вложенность структур, объединений и массивов друг в друга.

Тип реализующей ЭВМ: IBM PC-совмест. ПК

Язык программирования: OCaml

Вид и версия операционной системы: Linux

Объем программы для ЭВМ: 125 Кб