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

Материал из Кафедра математической кибернетики
Перейти к: навигация, поиск
м (Доклады на спецсеминарах)
(Доклады на спецсеминарах)
Строка 35: Строка 35:
 
|-
 
|-
 
|colspan="3"|'''[[Теоретические проблемы программирования]]'''
 
|colspan="3"|'''[[Теоретические проблемы программирования]]'''
{{announce Seminar| 7 апреля 2017 г.
+
{{announce Seminar| 29 сентября 2017 г.
| '''Проверка эквивалентности программ с неинтерпретируемыми функциями и целочисленной арифметикой'''.
+
| '''Верификация преобразований исходных кодов программ посредством проверки эквивалентности'''.
  
 
Доклад по статье N.P. Lopes, J. Monteiro "Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic"
 
Доклад по статье N.P. Lopes, J. Monteiro "Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic"
  
Доказательство эквивалентности программ имеет несколько важных приложений, в таких отраслях, как алгоритмы распознавания, регрессионное тестирование, тестирование сделанных компилятором оптимизаций и проверка утечек потоков информации. Несмотря на то что данная тема обладает важными приложениями, наука в проверки программ на эквивалентность не достигла серьёзных успехов за последние десятилетие в виду сложности этой задачи. В рассматриваемой статье предложен первая полуразрешающая процедура для автоматической проверки частичной эквивалентности двух программ, использующих неинтерпретируемые функции и работающих над целочисленной арифметикой (UF + IA). Предлагаемый алгоритм применим, в частности, к программам с вложенными циклами. Вначале проводится преобразование неинтерпретируемых функций (UF) в целочисленные полиномы, которые позволяют точно суммировать циклы с вхождениями UF, использующих рекурсию. Затем алгоритм проверки на эквивалентность переходит к свободным от циклов программам, оперирующих только целыми числами.
+
Доклад по статье K.C. Shashidhar, Maurice Bruynooghe, Francky Catthoor, Gerda Janssens "Verification of Source Code Transformations by Program Equivalence Checking"
| Е.М. Винарский, В.В. Подымов }}
+
  
 +
Как правило, когда алгоритмы для обработки цифровых сигналов адаптируются для работы в энергоэффективных и эффективно функционирующих встроенных системах, применяется комбинация ручных и автоматических преобразований. Это порождает сложную задачу верификации. Задача верификации упрощается при конвертирования кода в DSA-форму (dynamic single assignment form). Данная статья описывает метод доказательства эквивалентности двух программ в DSA-форме, в которых индексация элементов массивов и условия завершения циклов являются (кусочно заданными) аффинными выражениями. Для таких программ может быть использовано геометрическое моделирование и сразу для наборов элементов может быть показано, что результат вычислений обеих программ представляет собой одну и ту же функцию от входных данных.
 +
| М.М. Аббас }}
  
 +
{{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"
 +
 +
В этой статье показано, что для одной разновидности конечных временных автоматов с ограничениями на сроки обработки входного сигнала, задержкой выходного сигнала и тайм-аутом задача минимизации автоматов по числу состояний может быть сведена к аналогичной задаче для конечных детерминированных синхронных автоматов Мили.
 +
 +
| Е.М. Винарский }}
 
<!--
 
<!--
 
|-
 
|-

Версия 19:43, 28 сентября 2017

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

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



Сложность решения дискретных задач
Теоретические проблемы программирования
29 сентября 2017 г. Верификация преобразований исходных кодов программ посредством проверки эквивалентности.

Доклад по статье N.P. Lopes, J. Monteiro "Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic"

Доклад по статье 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 г. Рещение задачи минимизации для одного вида детерминированных временных автоматов.

Доклад по статье 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"

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


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