|
|
| (не показаны 98 промежуточные версии 6 участников) |
| Строка 2: |
Строка 2: |
| | {| | | {| |
| | |colspan="3"|'''[[Дискретная математика и математическая кибернетика]]''' | | |colspan="3"|'''[[Дискретная математика и математическая кибернетика]]''' |
| − | {{announce Seminar| | + | <!-- |
| − | | | + | {{announce Seminar | 6 ноября 2020 |
| − | | }} | + | | '''О возможностях построения легкотестируемых контактных схем и схем из функциональных элементов'''. |
| | + | Аннотация. Исследованы задачи реализации булевых функций контактными схемами и схемами из функциональных элементов, допускающими короткие проверяющие либо диагностические тесты относительно неисправностей заранее оговоренного вида, которые могут происходить в схемах. Указанные задачи были впервые предложены (применительно к контактным схемам) С.В. Яблонским |
| | + | и И.А. Чегис в середине 1950-х годов и изучались многими авторами. Рассмотрены следующие виды неисправностей: обрывы и/или замыкания контактов, константные (однотипные или произвольные) либо инверсные неисправности на входах и/или выходах функциональных элементов. Число допустимых неисправностей в схемах может быть ограничено сверху единицей или заданным натуральным числом либо никак не ограничено. Получен ряд верхних и/или нижних оценок длин минимальных тестов для схем, реализующих заданные, все или почти все булевы функции, при различных исходных условиях. Во многих случаях найдены точные значения этих длин и/или улучшены известные ранее результаты. |
| | + | | '''Попков К.А.''' (Институт прикладной математики им. М.В. Келдыша РАН)}} |
| | + | --> |
| | | | |
| | |- | | |- |
| | |colspan="3"|'''[[Дискретные функции и сложность алгоритмов]]''' | | |colspan="3"|'''[[Дискретные функции и сложность алгоритмов]]''' |
| − | {{announce Seminar| | + | {{announce Seminar| |
| | | | | | |
| | | }} | | | }} |
| | | | |
| | |- | | |- |
| − | |colspan="3"|'''[[Дискретный анализ]]''' | + | |colspan="3"|'''[[Теория управляющих систем и математические модели СБИС]]''' |
| | {{announce Seminar| | | {{announce Seminar| |
| | | | | | |
| | | }} | | | }} |
| − |
| |
| − | |-
| |
| − | |colspan="3"|'''[[Теория управляющих систем и математические модели СБИС]]''' и '''[[Некоторые вопросы теории управляющих систем]]'''
| |
| − | {{announce Seminar| 22 сентября 2017 г.
| |
| − | | Доклад «Cинтез рекурсивных схем из функциональных элементов»
| |
| − | | align="center" | Жуков В.В.
| |
| − | |}}
| |
| − |
| |
| − |
| |
| | | | |
| | |- | | |- |
| Строка 35: |
Строка 30: |
| | |- | | |- |
| | |colspan="3"|'''[[Теоретические проблемы программирования]]''' | | |colspan="3"|'''[[Теоретические проблемы программирования]]''' |
| − | {{announce Seminar| 6 октября 2017 г. | + | {{announce Seminar| |
| − | | '''Система правил для динамической верификации трасс событий'''. | + | | |
| − | | + | | }} |
| − | Доклад по статье H. Barringer, A. Goldberg, K. Havelund, K. Sen "Rule-Based Runtime Verification"
| + | |
| − | | + | |
| − | В статье описываются принципы работы программного средства, решающего следующую задачу. Имеется программа, работающая в режиме "чёрного ящика". В программе включен отладочный вывод: время от времени она предоставляет сообщения, содержащие информацию о значениях некоторых переменных. Требуется проверить, удовлетворяет ли текущая посланная последовательность сообщений заданным требованиям, в режиме он-лайн: выдавать результаты о выполнении требований по мере получения сообщений. Для решения этой задачи авторами предлагается особый логический формализм (Eagle): система правил, с одной стороны являющихся элементами синтаксиса формул, а с другой - описывающих способ перевычисления информации об истинности формул в режиме он-лайн. В предлагаемом формализме могут быть легко переформулированы требования, изначально записанные в ряде других известных логик, включая произвольные требования, выраженные формулами логики линейного прошлого времени (past-time LTL). Этот формализм и будет обсуждаться на семинаре.
| + | |
| − | | В.В. Подымов }} | + | |
| − | | + | |
| − | {{announce Seminar| 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-форме, в которых индексация элементов массивов и условия завершения циклов являются (кусочно заданными) аффинными выражениями. Для таких программ может быть использовано геометрическое моделирование и сразу для наборов элементов может быть показано, что результат вычислений обеих программ представляет собой одну и ту же функцию от входных данных.
| + | |
| − | | М.М. Аббас }}
| + | |
| − | | + | |
| − | {{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"
| + | |
| − | | + | |
| − | В этой статье показано, что для одной разновидности конечных временных автоматов с ограничениями на сроки обработки входного сигнала, задержкой выходного сигнала и тайм-аутом задача минимизации автоматов по числу состояний может быть сведена к аналогичной задаче для конечных детерминированных синхронных автоматов Мили.
| + | |
| − | | + | |
| − | | Е.М. Винарский }}
| + | |
| − | <!--
| + | |
| − | |-
| + | |
| − | |colspan="3"|'''[[Просеминар для 2-го курса]]'''
| + | |
| − | {{announce Seminar||| }}
| + | |
| − | -->
| + | |
| | |} | | |} |
