Шаблон:Current Seminars

Доклады на спецсеминарах

Дискретная математика и математическая кибернетика
Дискретные функции и сложность алгоритмов
Дискретный анализ
Теория управляющих систем и математические модели СБИС и Некоторые вопросы теории управляющих систем
22 сентября 2017 г.	Доклад «Cинтез рекурсивных схем из функциональных элементов»	Жуков В.В.
Сложность решения дискретных задач
13 октября 2017 г.	NP-полнота некоторых задач о раскраске графов без заданных порожденных подграфов: о раскраске в 4 цвета графа без порожденных цепей с 8 вершинами; о предраскраскраске в 4 цвета графа без порожденных цепей с 7 вершинами. Доклад по статье: Broesma H., Golovach P.A., Paulusma D., Song J. Updating the complexity status of coloring graphs without a fixed induced linear forest.	Сакович Марк, 418 гр.
6 октября 2017 г.	NP-полнота некоторых задач о раскраске графов: о раскраске графа в 3 цвета; о раскраске в 3 цвета графа со степенями вершин, не более 4; о раскраске в 3 цвета планарного графа.	Мельник Марина, 618/1 гр.
Теоретические проблемы программирования
6 октября 2017 г.	Система правил для динамической верификации трасс событий. Доклад по статье H. Barringer, A. Goldberg, K. Havelund, K. Sen "Rule-Based Runtime Verification" В статье описываются принципы работы программного средства, решающего следующую задачу. Имеется программа, работающая в режиме "чёрного ящика". В программе включен отладочный вывод: время от времени она предоставляет сообщения, содержащие информацию о значениях некоторых переменных. Требуется проверить, удовлетворяет ли текущая посланная последовательность сообщений заданным требованиям, в режиме он-лайн: выдавать результаты о выполнении требований по мере получения сообщений. Для решения этой задачи авторами предлагается особый логический формализм (Eagle): система правил, с одной стороны являющихся элементами синтаксиса формул, а с другой - описывающих способ перевычисления информации об истинности формул в режиме он-лайн. В предлагаемом формализме могут быть легко переформулированы требования, изначально записанные в ряде других известных логик, включая произвольные требования, выраженные формулами логики линейного прошлого времени (past-time LTL). Этот формализм и будет обсуждаться на семинаре.	В.В. Подымов
29 сентября 2017 г.	Верификация преобразований исходных кодов программ посредством проверки эквивалентности. Доклад по статье K.C. Shashidhar, Maurice Bruynooghe, Francky Catthoor, Gerda Janssens "Verification of Source Code Transformations by Program Equivalence Checking" Как правило, когда алгоритмы для обработки цифровых сигналов адаптируются для работы в энергоэффективных и эффективно функционирующих встроенных системах, применяется комбинация ручных и автоматических преобразований. Это порождает сложную задачу верификации. Задача верификации упрощается при конвертирования кода в DSA-форму (dynamic single assignment form). Данная статья описывает метод доказательства эквивалентности двух программ в DSA-форме, в которых индексация элементов массивов и условия завершения циклов являются (кусочно заданными) аффинными выражениями. Для таких программ может быть использовано геометрическое моделирование и сразу для наборов элементов может быть показано, что результат вычислений обеих программ представляет собой одну и ту же функцию от входных данных.	М.М. Аббас
22 сентября 2017 г.	Рещение задачи минимизации для одного вида детерминированных временных автоматов. Доклад по статье Aleksandr Tvardovskii, Nina Yevtushenko "On minimization of Timed Finite State Machines" В этой статье показано, что для одной разновидности конечных временных автоматов с ограничениями на сроки обработки входного сигнала, задержкой выходного сигнала и тайм-аутом задача минимизации автоматов по числу состояний может быть сведена к аналогичной задаче для конечных детерминированных синхронных автоматов Мили.	Е.М. Винарский