Modern trends in discrete mathematics and computer science — различия между версиями

Материал из Кафедра математической кибернетики
Перейти к: навигация, поиск
Строка 9: Строка 9:
 
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.
 
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.
  
−
== Lecture 1. '''[[Media: LectEng1.pdf| Theory and practice of software obfuscation.]]''' ==
+
= Preliminary program and materials =
 +
 
 +
== Lecture 1. '''Theory and practice of software obfuscation.''' ==
 +
 
 +
[[Media: LectEng1.pdf|Presentation.]]
  
 
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.  
 
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'''.
+
Lecturer: '''Vladimir Zakharov'''.
 +
 
 +
== Lecture 2. '''Formal correctness proofs for sequential programs.''' ==
 +
 
 +
This lecture is devoted to formal verification of sequential imperative programs.
 +
The main topic of the lecture is the notion of formal system (logical calculus) applied to correctness proof for imperative programs.
 +
Several valuable properties of such formal systems and proofs for simple-but-useful programs are to be discussed.
 +
 
 +
Lecturer: '''Vladislav Podymov'''.
 +
 
 +
== Lectures 3,4. '''Constraint satisfaction problem: an algebraic approach.''' ==
 +
 
 +
== Lecture 5. '''Closed classes in k-valued and partial k-valued logics.''' ==
 +
 
 +
== Lecture 6. '''Read-once functions.''' ==
 +
 
 +
== Lecture 7. '''Some new bounds of Shannon functions for cardinality of test sets for logical circuits.''' ==
  
−
# '''Formal correctness proofs for sequential programs.'''
+
== Lecture 8. '''13С metabolic flux analysis.''' ==
−
#* Лекция посвящена изучению и обсуждению дедуктивных методов верификации (проверки корректности) последовательных императивных программ. В лекции рассматриваются полезные свойства формальных систем верификации программ и примеры их применения к проверке правильности небольших программ.
+
−
# '''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). В рамках лекции предполагается рассмотреть основные подходы к моделированию перераспределения тяжелых атомов углерода в процессе жизнедеятельности клетки, а также основные методы решения задачи определения метаболических потоков.
+
  
−
== Literature ==
+
= Literature =
  
 
# Варновский Н.П., Захаров В.А., Кузюрин Н.П., Шокуров А.В. Современное состояние исследований в области обфускации программ: определения стойкости обфускации // Труды института системного программирования, 2014б т. 26, вып. 3, с. 167-191.
 
# Варновский Н.П., Захаров В.А., Кузюрин Н.П., Шокуров А.В. Современное состояние исследований в области обфускации программ: определения стойкости обфускации // Труды института системного программирования, 2014б т. 26, вып. 3, с. 167-191.
 
# Cappaert J. Code Obfuscation Techniques for Software Protection. PhD Thesis, 2012, Leuven University.
 
# Cappaert J. Code Obfuscation Techniques for Software Protection. PhD Thesis, 2012, Leuven University.

Версия 19:04, 10 февраля 2018


Compulsory course for master students, 2-nd year, groups 618/1 and 618/2.

Lectures — 16 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.

Preliminary program and materials

Lecture 1. Theory and practice of software obfuscation.

Presentation.

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.

Lecture 2. Formal correctness proofs for sequential programs.

This lecture is devoted to formal verification of sequential imperative programs. The main topic of the lecture is the notion of formal system (logical calculus) applied to correctness proof for imperative programs. Several valuable properties of such formal systems and proofs for simple-but-useful programs are to be discussed.

Lecturer: Vladislav Podymov.

Lectures 3,4. Constraint satisfaction problem: an algebraic approach.

Lecture 5. Closed classes in k-valued and partial k-valued logics.

Lecture 6. Read-once functions.

Lecture 7. Some new bounds of Shannon functions for cardinality of test sets for logical circuits.

Lecture 8. 13С metabolic flux analysis.

Literature

  1. Варновский Н.П., Захаров В.А., Кузюрин Н.П., Шокуров А.В. Современное состояние исследований в области обфускации программ: определения стойкости обфускации // Труды института системного программирования, 2014б т. 26, вып. 3, с. 167-191.
  2. Cappaert J. Code Obfuscation Techniques for Software Protection. PhD Thesis, 2012, Leuven University.
Источник — «https://mk.cs.msu.ru/index.php?title=Modern_trends_in_discrete_mathematics_and_computer_science&oldid=4807»