Modern trends in discrete mathematics and computer science — различия между версиями
Материал из Кафедра математической кибернетики
| Строка 9: | Строка 9: | ||
Responsible lecturer [[Захаров Владимир Анатольевич|Vladimir Zakharov]]. | Responsible lecturer [[Захаров Владимир Анатольевич|Vladimir Zakharov]]. | ||
| + | This course is intended to introduce the audience to some topics in discrete mathematics and its applications in software engineering, VLSI designing and biochemistry which are in line with the modern development of computer science and applied mathematics. | ||
| − | = | + | == Program of the course == |
| + | |||
| + | == Lecture 1. == | ||
| + | |||
| + | '''[[Media: LectEng1.pdf| Theory and practice of software obfuscation.]]''' == | ||
| + | |||
| + | This lecture is devoted to the software obfuscation problem, its applications in software protection, information hiding and cryptography, to the practical techniques of program obfuscation with the help of structures and techniques from discrete mathematics, automata theory, coding theory. Much attention is payed to formal definitions of obfuscation security. It wil be shown that a secure obfuscation of some programs is impossible in the framework of a "black box" model, but , nevertheless, certain classes of simple programs admit secure obfuscation. | ||
| + | |||
| + | Lecturer '''Vladimir Zakharov'''. | ||
| − | |||
| − | |||
# '''Formal correctness proofs for sequential programs.''' | # '''Formal correctness proofs for sequential programs.''' | ||
#* Лекция посвящена изучению и обсуждению дедуктивных методов верификации (проверки корректности) последовательных императивных программ. В лекции рассматриваются полезные свойства формальных систем верификации программ и примеры их применения к проверке правильности небольших программ. | #* Лекция посвящена изучению и обсуждению дедуктивных методов верификации (проверки корректности) последовательных императивных программ. В лекции рассматриваются полезные свойства формальных систем верификации программ и примеры их применения к проверке правильности небольших программ. | ||
Версия 17:48, 10 февраля 2018
Актуальность информации: весенний семестр 2017/2018 учебного года
Compulsory course master students, groups 618/1 and 618/2.
Lectures — 48 h.
Responsible lecturer Vladimir Zakharov.
This course is intended to introduce the audience to some topics in discrete mathematics and its applications in software engineering, VLSI designing and biochemistry which are in line with the modern development of computer science and applied mathematics.
Program of the course
Lecture 1.
Theory and practice of software obfuscation. ==
This lecture is devoted to the software obfuscation problem, its applications in software protection, information hiding and cryptography, to the practical techniques of program obfuscation with the help of structures and techniques from discrete mathematics, automata theory, coding theory. Much attention is payed to formal definitions of obfuscation security. It wil be shown that a secure obfuscation of some programs is impossible in the framework of a "black box" model, but , nevertheless, certain classes of simple programs admit secure obfuscation.
Lecturer Vladimir Zakharov.
- Formal correctness proofs for sequential programs.
- Лекция посвящена изучению и обсуждению дедуктивных методов верификации (проверки корректности) последовательных императивных программ. В лекции рассматриваются полезные свойства формальных систем верификации программ и примеры их применения к проверке правильности небольших программ.
- Constraint satisfaction problem: an algebraic approach.
- Задача удовлетворения ограничений состоит в выяснении выполнимости системы отношений. При этом отношения принадлежат заранее известному множеству S и зависят от произвольных переменных. В русскоязычной литературе она также называется задачей обобщенной выполнимости. Многочисленные вопросы информатики (в частности, в распознавании образов, анализе программ, представлении знаний, базах данных) и дискретной математики (например, раскраски графов) естественным образом выражаются в терминах этой задачи. Перспективным подходом к ее решению считается алгебраический подход. Он состоит в рассмотрении функций, сохраняющих все отношения из множества S. В зависимости от вида этих функций можно показать либо полиномиальность, либо NP-полноту соответствующей задачи. В двух лекциях предполагается определить задачу удовлетворения ограничений, показать примеры ее применения, описать алгебраический подход к ее решению и рассказать о полученных с его помощью результатах, в том числе совсем новых.
- Closed classes in k-valued and partial k-valued logics.
- В лекции приводится обзор результатов по описанию фрагментов решетки замкнутых классов (относительно суперпозиции) в k-значной и частичной k-значной логиках и рассказано о последних достижениях в этой области. Будут представлены результаты о предполных классах в k-значной и частичной k-значной логиках, о замкнутых классах в k-значной логике, содержащих класс Слупецкого или все полиномы, о замкнутых классах в частичной k-значной логике, содержащих заданный предполный класс k-значной логики.
- Read-once functions.
- Основной объект изучения - булевы функции, представимые формулами без повторения аргументов. Рассматриваются вопросы тестирования и расшифровки функций (в том числе мощными оракулами). Также рассматривается схемное распознавание свойства бесповторности и сертификатное доказательство повторности функций.
- Some new bounds of Shannon functions for cardinality of test sets for logical circuits.
- В лекции будет рассказано о современном состоянии той части теории контроля логических схем, которая связана с изучением поведения функций Шеннона длин тестов (то есть длин минимальных тестов для самых труднотестируемых функций).
- 13С metabolic flux analysis.
- Изотопные эксперименты с тяжелыми атомами углерода (13С metabolic flux analysis) являются распространенным методом анализа скоростей метаболических реакций, так называемых «потоков» (13С metabolic flux analysis). В рамках лекции предполагается рассмотреть основные подходы к моделированию перераспределения тяжелых атомов углерода в процессе жизнедеятельности клетки, а также основные методы решения задачи определения метаболических потоков.
