Конференция, посвященная 90-летию со дня рождения Алексея Андреевича Ляпунова

Россия, Новосибирск, Академгородок, 8 - 11 октября 2001 года,
(номер государственной регистрации 0320300063)

Тезисы докладов

Программирование

На пути к верификации С-программ. Язык C-light.

Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В.

Институт систем информатики СО РАН (Новосибирск)

Описано ориентированное на верификацию представительное подмножество языка C --- язык C-light. Этот язык допускает детерминированные выражения, ограниченное использование операторов switch и goto, а вместо библиотечных функций для работы с динамической памятью включает операции new и delete языка C++. Для языка C-light представлена структурная операционная семантика в стиле Плоткина. Язык C-light служит входным языком разрабатываемой верификации.

Дополнительные материалы: HTML
Примечание. Тезисы докладов публикуются в авторской редакции

Ваши комментарии

[Головная страница]
[Конференции]
[СО РАН]

© 2001, Сибирское отделение Российской академии наук, Новосибирск
© 2001, Объединенный институт информатики СО РАН, Новосибирск
© 2001, Институт вычислительных технологий СО РАН, Новосибирск
© 2001, Институт систем информатики СО РАН, Новосибирск
© 2001, Институт математики СО РАН, Новосибирск
© 2001, Институт цитологии и генетики СО РАН, Новосибирск
© 2001, Институт вычислительной математики и математической геофизики СО РАН, Новосибирск
© 2001, Новосибирский государственный университет
Дата последней модификации 06-Jul-2012 (11:45:21)