Шаблон:Current Seminars — различия между версиями

Материал из Кафедра математической кибернетики
Перейти к: навигация, поиск
м (Доклады на спецсеминарах)
Строка 53: Строка 53:
 
{{announce Seminar| 22 сентября 2017 г.
 
{{announce Seminar| 22 сентября 2017 г.
 
| '''Рещение задачи минимизации для одного вида детерминированных временных автоматов'''.
 
| '''Рещение задачи минимизации для одного вида детерминированных временных автоматов'''.
 
Доклад по статье N.P. Lopes, J. Monteiro "Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic"
 
  
 
Доклад по статье Aleksandr Tvardovskii, Nina Yevtushenko "On minimization of Timed Finite State Machines"
 
Доклад по статье Aleksandr Tvardovskii, Nina Yevtushenko "On minimization of Timed Finite State Machines"

Версия 17:57, 4 октября 2017

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

Дискретная математика и математическая кибернетика
Дискретные функции и сложность алгоритмов
Дискретный анализ
Теория управляющих систем и математические модели СБИС и Некоторые вопросы теории управляющих систем
22 сентября 2017 г. Доклад «Cинтез рекурсивных схем из функциональных элементов» Жуков В.В.



Сложность решения дискретных задач
Теоретические проблемы программирования
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"

В этой статье показано, что для одной разновидности конечных временных автоматов с ограничениями на сроки обработки входного сигнала, задержкой выходного сигнала и тайм-аутом задача минимизации автоматов по числу состояний может быть сведена к аналогичной задаче для конечных детерминированных синхронных автоматов Мили.


Е.М. Винарский