Версия 17:24, 10 февраля 2018

Актуальность информации: весенний семестр 2017/2018 учебного года

Compulsory course master students, groups 618/1 and 618/2.

Lectures — 48 h.

Responsible lecturer Vladimir Zakharov.

Предварительная программа курса

1. Theory and practice of software obfuscation.
   • В этой лекции рассказывается о задаче обфускации программ, о практических приемах обфускации с применением конструкций и методов дискретной математики, теории автоматов, теории кодирования. Приводятся математические определения стойкости обфускации программ. Доказываются теоремы о невозможности построения стойкого обфускатора программ в модели «черного ящика», и о возможности стойкой обфускации программ, вычисляющих некоторые классы функций.
2. Formal correctness proofs for sequential programs.
   • Лекция посвящена изучению и обсуждению дедуктивных методов верификации (проверки корректности) последовательных императивных программ. В лекции рассматриваются полезные свойства формальных систем верификации программ и примеры их применения к проверке правильности небольших программ.
3. Constraint satisfaction problem: an algebraic approach.
   • Задача удовлетворения ограничений состоит в выяснении выполнимости системы отношений. При этом отношения принадлежат заранее известному множеству S и зависят от произвольных переменных. В русскоязычной литературе она также называется задачей обобщенной выполнимости. Многочисленные вопросы информатики (в частности, в распознавании образов, анализе программ, представлении знаний, базах данных) и дискретной математики (например, раскраски графов) естественным образом выражаются в терминах этой задачи. Перспективным подходом к ее решению считается алгебраический подход. Он состоит в рассмотрении функций, сохраняющих все отношения из множества S. В зависимости от вида этих функций можно показать либо полиномиальность, либо NP-полноту соответствующей задачи. В двух лекциях предполагается определить задачу удовлетворения ограничений, показать примеры ее применения, описать алгебраический подход к ее решению и рассказать о полученных с его помощью результатах, в том числе совсем новых.
4. Closed classes in k-valued and partial k-valued logics.
   • В лекции приводится обзор результатов по описанию фрагментов решетки замкнутых классов (относительно суперпозиции) в k-значной и частичной k-значной логиках и рассказано о последних достижениях в этой области. Будут представлены результаты о предполных классах в k-значной и частичной k-значной логиках, о замкнутых классах в k-значной логике, содержащих класс Слупецкого или все полиномы, о замкнутых классах в частичной k-значной логике, содержащих заданный предполный класс k-значной логики.
5. Read-once functions.
   • Основной объект изучения - булевы функции, представимые формулами без повторения аргументов. Рассматриваются вопросы тестирования и расшифровки функций (в том числе мощными оракулами). Также рассматривается схемное распознавание свойства бесповторности и сертификатное доказательство повторности функций.
6. Some new bounds of Shannon functions for cardinality of test sets for logical circuits.
   • В лекции будет рассказано о современном состоянии той части теории контроля логических схем, которая связана с изучением поведения функций Шеннона длин тестов (то есть длин минимальных тестов для самых труднотестируемых функций).
7. 13С metabolic flux analysis.
   • Изотопные эксперименты с тяжелыми атомами углерода (13С metabolic flux analysis) являются распространенным методом анализа скоростей метаболических реакций, так называемых «потоков» (13С metabolic flux analysis). В рамках лекции предполагается рассмотреть основные подходы к моделированию перераспределения тяжелых атомов углерода в процессе жизнедеятельности клетки, а также основные методы решения задачи определения метаболических потоков.