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

Материал из Кафедра математической кибернетики
Перейти к: навигация, поиск
(Доклады на спецсеминарах)
(Доклады на спецсеминарах)
Строка 38: Строка 38:
 
|-
 
|-
 
|colspan="3"|'''[[Теоретические проблемы программирования]]'''
 
|colspan="3"|'''[[Теоретические проблемы программирования]]'''
{{announce Seminar| 31 марта 2017 г.
+
{{announce Seminar| 7 апреля 2017 г.
| '''Распознавание вредоносных программ на основе их семантического анализа'''.
+
| '''Проверка эквивалентности программ с неинтерпретируемыми функциями и целочисленной арифметикой'''.
 +
.
  
Доклад по статье M.Christodorescu et al. "Semantics-aware malware detection"
+
Доклад по статье N.P. Lopes, J. Monteiro "Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic"
  
Вирусы разрабатываются так, чтобы существовать во множестве вариантов, препятствующих их обнаружению в коде зараженного файла по какой-то конкретной последовательности байт. В статье предлагается искать вирус по шаблонам моделирующим некоторое характерное для вирусов поведение. Показано что задача проверки совпадения такого шаблона в общем случае неразрешима. Предложен и программно реализован алгоритм успешно обнаруживающий некоторые семейства вирусов.
+
Доказательство эквивалентности программ имеет несколько важных приложений, в таких отраслях, как алгоритмы распознавания, регрессионное тестирование, тестирование сделанных компилятором оптимизаций и проверка утечек потоков информации. Несмотря на то что данная тема обладает важными приложениями, наука в проверки программ на эквивалентность не достигла серьёзных успехов за последние десятилетие в виду сложности этой задачи. В рассматриваемой статье предложен первая полуразрешающая процедура для автоматической проверки частичной эквивалентности двух программ, использующих неинтерпретируемые функции и работающих над целочисленной арифметикой (UF + IA). Предлагаемый алгоритм применим, в частности, к программам с вложенными циклами. Вначале проводится преобразование неинтерпретируемых функций (UF) в целочисленные полиномы, которые позволяют точно суммировать циклы с вхождениями UF, использующих рекурсию. Затем алгоритм проверки на эквивалентность переходит к свободным от циклов программам, оперирующих только целыми числами.
| М.Аббас, П.Булгаков }}
+
| Е.М. Винарский, В.В. Подымов }}
  
  

Версия 18:18, 1 апреля 2017

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

Дискретная математика и математическая кибернетика
Дискретные функции и сложность алгоритмов
Дискретный анализ
Теория управляющих систем и математические модели СБИС
17 марта 2017 г. ауд. 507 Доклад по статьям, связанным с некоторыми модификациями теоремы В. М. Храпченко.Аннотация доклада Трубицын Ю.А.
Некоторые вопросы теории управляющих систем
17 марта 2017 г. ауд. 582а Доклад по статье Евдокимова А.А. «О максимальной длине цепи в единичном n-мерном кубе».Аннотация доклада Козловский А.Н.
Сложность решения дискретных задач
Теоретические проблемы программирования
7 апреля 2017 г. Проверка эквивалентности программ с неинтерпретируемыми функциями и целочисленной арифметикой.

.

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

Доказательство эквивалентности программ имеет несколько важных приложений, в таких отраслях, как алгоритмы распознавания, регрессионное тестирование, тестирование сделанных компилятором оптимизаций и проверка утечек потоков информации. Несмотря на то что данная тема обладает важными приложениями, наука в проверки программ на эквивалентность не достигла серьёзных успехов за последние десятилетие в виду сложности этой задачи. В рассматриваемой статье предложен первая полуразрешающая процедура для автоматической проверки частичной эквивалентности двух программ, использующих неинтерпретируемые функции и работающих над целочисленной арифметикой (UF + IA). Предлагаемый алгоритм применим, в частности, к программам с вложенными циклами. Вначале проводится преобразование неинтерпретируемых функций (UF) в целочисленные полиномы, которые позволяют точно суммировать циклы с вхождениями UF, использующих рекурсию. Затем алгоритм проверки на эквивалентность переходит к свободным от циклов программам, оперирующих только целыми числами.

Е.М. Винарский, В.В. Подымов