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

Понедельник 14 июня 2010

Время
08:30-09:45 Регистрация
09:45-10:00 Открытие семинара
Заседание 1 Председатель Шилов Н.В.
10:00-10:30 Башкин В.А. «Об использовании однопериодических базисов для глобальной символьной верификации»
10:30-11:00 Башкин В.А., Ломазова И.А. «Двухуровневое моделирование мультиагентных систем на основе обобщенных сетей активных ресурсов»
11:00-11:30 Валиев М.К., Дехтярь М.И. «Сложность верификации недетерминированных вероятностных мультиагентных систем»
11:30-12:00 Кузьмин Е. В., Соколов В. А., Чалый Д. Ю. «О языках автоматных счетчиковых машин»
12:00-14:00 Ланч
Заседание 2 Председатель Соколов В.А.
14:00-14:30 Konnov I.V. «Using adaptive symmetry reduction for LTL model checking»
14:30-15:00 Гаранина Н.О. «Аффинное представление данных для символьной проверки моделей распределенных систем»
15:00-15:30 Подловченко Р. И. «Методология построения системы эквивалентных преобразований, полной в модели вычислений, и ее применение для алгебраических моделей программ»
15:30-16:00 Кофе-брейк
Заседание 3 Стендовые доклады Председатель Промский А.В.
16:00-17:30 Anikeev M., Madlener F., Schlosser A., Huss S. A., Walther Ch. «A Viable Approach to Machine-Checked Correctness Proof of Algorithm Variants in Elliptic Curve Cryptography»
Беляев А.Б. «Верификация алгоритма поддержки транзакционной памяти»
Давыдов А.В., Ларионов А.А. «Об исчислении позитивно-образованных формул для автоматического доказательства теорем»
Калентьев А.А., Тюгашев А. А., Шулындин А.В. «Формальная верификация требований к управляющим алгоритмам реального времени»
Клебанов А. А., Степанов О. Г., Шалыто А. А. «Применение шаблонов требований к формальной спецификации и верификации автоматных программ»
Клепнин А.В., Мелентьев А.А. «Интеграция семантических верификаторов в компиляторы языка Java»
Мальшаков Г.В. «Верификация объединения подсистем автоматизации вуза»
Федотов В.Н. «Сервисно-ориентированный подход к тестированию интеграции в распределенных системах»
Шелехов В.И. «Верификация и синтез программ сложения на базе правил корректности операторов»
Шилов Н.В. «Пример верификации в проекте F@BOOL@»

Вторник 15 июня 2010

Время
Заседание 4 Председатель Кулямин В.В.
10:00-10:30 Letichevsky A.A., Letychevskyi O.A., Weigert T. «Predicate transformers for symbolic verification»
10:30-11:00 Котляров В.П., Дробинцев П.Д. «Формальный подход к проверке качества программных продуктов»
11:00-11:30 Непомнящий В.А., Ануреев И.С., Атучин М.М., Марьясов И.В., Петров А.А., Промский А.В. «Система анализа и верификации С-программ СПЕКТР-2»
11:30-12:00 Шошмина И.В., Карпов Ю.Г. «Технология проектирования и верификации распределенных бортовых систем»
12:00-14:00 Ланч
Заседание 5
14:00-14:30 Батаев А.В., Давыдов А.А., Налютин Н.Ю., Синицын С.В. «Метод генерации тестовых данных на основе формальных спецификаций»
14:30-15:00 Бурдонов И.Б., Косачев А.С. «Симуляция систем с отказами и разрушением»
15:00-15:30 Бурдонов И.Б., Косачев А.С. «Тестирование безопасной симуляции»
15:30-16:00 Кофе-брейк
Заседание 6
16:00-17:30 Панельная дискуссия. Председатель Непомнящий В.А.
Панельная дискуссия «Актуальные задачи верификации программ. От теории к приложениям». Участники: Кулямин В.В., Летичевский А.А., Соколов В.А., Шилов Н.В.