Программа генерации монадического представления Си-программ
ФУНКЦИОНАЛЬНОЕ ПРОГРАММИРОВАНИЕ, МОНАДИЧЕСКОЕ ПРЕДСТАВЛЕНИЕ, ВЕРИФИКАЦИя ПРОГРАММ
Программа предназначена для трансляции программ, написанных на языке Си в монадическое представление,  сохраняемое в формате JSON. Механизм трансляции опирается на промежуточное CIL представление языка Си и сохраняет большое количество метаданных. Также при трансляции используется алгоритм выделения циклических блоков, чтобы привести все циклы в вид, пригодный для генерации рекурсивных функций. Программа применятся в качестве первого шага процедуры трансляции Си кода в логическую модель на языке Isabelle/HOL.
Дедуктивная верификация программ на языке Си.
Петренко А. К.
заведующий отделом
Доктор физико-математических наук
Аветисян А. И.
ВРИО директора
50.05.17
Теоретические основы системного программного обеспечения
01.02.ET
COMPUTER SCIENCE, INFORMATION SYSTEMS
01.02.EX
COMPUTER SCIENCE, THEORY & METHODS
01.02.EW
COMPUTER SCIENCE, SOFTWARE ENGINEERING
Михаил
Мандрыкин
Усамович
Проектирование алгоритмов.
Павел
Путро
Андреевич
Проектирование, разработка и реализация алгоритмов. Написание и отладка программы.
МИНОБРНАУКИ РОССИИ
МИНИСТЕРСТВО НАУКИ И ВЫСШЕГО ОБРАЗОВАНИЯ РОССИЙСКОЙ ФЕДЕРАЦИИ
1187746579690
Организация
Министерство науки и высшего образования Российской Федерации
Федеральные государственные казенные учреждения
ИСП РАН
Федеральное государственное бюджетное учреждение науки Институт системного программирования им. В.П. Иванникова Российской академии наук
1037700067327
Организация
Министерство науки и высшего образования Российской Федерации
Федеральные государственные бюджетные учреждения