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

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

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

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

Дата публикации: 20.08.2016

Контактные реквизиты:
info-lvc@linuxtesting.org
	
Авторы:
Мандрыкин Михаил Усамович,
Хорошилов Алексей Владимирович

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

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

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

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

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

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

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