Шаблон:Current Seminars — различия между версиями
м (→Доклады на спецсеминарах) |
(→Доклады на спецсеминарах) |
||
| Строка 35: | Строка 35: | ||
|- | |- | ||
|colspan="3"|'''[[Теоретические проблемы программирования]]''' | |colspan="3"|'''[[Теоретические проблемы программирования]]''' | ||
| − | {{announce Seminar| | + | {{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" | ||
| − | + | Доклад по статье 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" В этой статье показано, что для одной разновидности конечных временных автоматов с ограничениями на сроки обработки входного сигнала, задержкой выходного сигнала и тайм-аутом задача минимизации автоматов по числу состояний может быть сведена к аналогичной задаче для конечных детерминированных синхронных автоматов Мили.
|
Е.М. Винарский |
