Научная работа — различия между версиями

Материал из Кафедра математической кибернетики
Перейти к: навигация, поиск
(Новая страница: «= Научные темы = == [http://istina.msu.ru/projects/16278047/ Изучение свойств и разработка алгоритмов для ди…»)
 
(Разработка математических моделей и методов верификации программ)
Строка 59: Строка 59:
  
 
== Разработка математических моделей и методов верификации программ ==
 
== Разработка математических моделей и методов верификации программ ==
'''''(проф. Р.И. Подловченко, проф. В.А. Захаров, м.н.с. В.В.Подымов)'''''
+
'''''(проф. В.А. Захаров, м.н.с. В.В.Подымов)'''''
  
 
Одной из центральных задач математической кибернетики является задача анализа поведения сложных информационных систем (микроэлектронных схем, компьютерных программ, сетевых протоколов и др.). Для решения этой задачи применяются математические модели и методы теории автоматов и формальных языков, алгебры, математической логики, теории булевых функций. Разработанные модели и методы применяются, в частности, для решения задачи верификации программ – проверки того, что вычисления программы удовлетворяют заданным требованиям, предъявляемым к ее поведению. Сотрудники кафедры математической кибернетики внесли существенный вклад в исследование этой задачи. Для решения проблем эквивалентности и эквивалентных преобразований программ была разработана и развита теория алгебраических моделей программ, на основе которой были созданы эффективные алгоритмы проверки эквивалентности программ и полные системы эквивалентных преобразований программ.  В тесном сотрудничестве с лабораторией вычислительных комплексов факультета ВМК и Институтом системного программирования РАН проводятся исследования в области обфускации (маскировки) программ, а также в области верификации распределенных программ и встроенных систем.
 
Одной из центральных задач математической кибернетики является задача анализа поведения сложных информационных систем (микроэлектронных схем, компьютерных программ, сетевых протоколов и др.). Для решения этой задачи применяются математические модели и методы теории автоматов и формальных языков, алгебры, математической логики, теории булевых функций. Разработанные модели и методы применяются, в частности, для решения задачи верификации программ – проверки того, что вычисления программы удовлетворяют заданным требованиям, предъявляемым к ее поведению. Сотрудники кафедры математической кибернетики внесли существенный вклад в исследование этой задачи. Для решения проблем эквивалентности и эквивалентных преобразований программ была разработана и развита теория алгебраических моделей программ, на основе которой были созданы эффективные алгоритмы проверки эквивалентности программ и полные системы эквивалентных преобразований программ.  В тесном сотрудничестве с лабораторией вычислительных комплексов факультета ВМК и Институтом системного программирования РАН проводятся исследования в области обфускации (маскировки) программ, а также в области верификации распределенных программ и встроенных систем.

Версия 09:59, 2 ноября 2016

Научные темы

Изучение свойств и разработка алгоритмов для дискретных структур и функциональных систем

(Руководитель проф. В.Б. Алексеев)

Цель и направления научных исследований: получение решеток замкнутых классов дискретных функций и изучение их свойств, описание характеристик дискретных функций, разработка быстрых алгоритмов для дискретных структур.

Теория дискретных управляющих систем, ее приложения в проектировании СБИС и программировании

(Руководители проф. В.А. Захаров, проф. C.А. Ложкин)

Теория дискретных управляющих систем является интенсивно развивающейся областью дискретной математики и математической кибернетики. Ее развитие обусловлено как появлением новых направлений (и, в частности, направления, связанного с получением асимптотических оценок высокой степени точности), так и прогрессом в традиционных направлениях (например, в разработке методов и алгоритмов анализа, верификации, тестирования и оптимизации различных моделей управляющих систем, включая модели СБИС и модели программ). С другой стороны, теоретические результаты, полученные в этой области, находят применение при решении различных прикладных задач. К их числу относятся задачи проектирования современных СБИС наноуровня, задачи проектирования и верификации распределенных информационных систем, задачи оптимизации программ.

Области научных интересов

Сложность вычислений

(проф. В.Б. Алексеев, проф. А.А. Вороненко, доц. С.Н. Селезнева)

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

Наряду с широко известными принципами построения эффективных алгоритмов, такими как «разделяй и властвуй», «динамическое программирование» и др., на кафедре разрабатываются новые. В.Б. Алексеевым развивается перспективная алгебраическая модель построения алгоритмов, опирающаяся на принцип «расширения модели», ведется сотрудничество с Маркусом Блейзером (Markus Bläser, Германия), работающим в области алгебраической сложности. На основе этой модели В.Б. Алексеевым получены линейные или почти линейные оценки сложности решения задач распознавания свойств дискретных функций. А.А. Вороненко найден алгоритм распознавания монотонности булевых функций с почти линейной оценкой сложности, также построен фрагмент теории тестирования булевых функций. С.Н. Селезневой найдены быстрые алгоритмы распознавания свойств многозначных функций.

Проводимые исследования были поддержаны грантами Российского фонда фундаментальных исследований и Федеральной целевой программой «Научные и научно-педагогические кадры инновационной России».

Спецсеминары: Дискретная математика и математическая кибернетика, Дискретные функции и сложность алгоритмов, Сложность решения дискретных задач.

Дискретные модели в задачах информатики

(проф. В.Б. Алексеев, проф. А.А. Вороненко, проф. С.С. Марченков, проф. А.А. Сапоженко, доц. С.Н. Селезнева, к.ф.-м.н. А.С. Нагорный)

На кафедре математической кибернетики разрабатываются и развиваются дискретные модели в применении к задачам информатики. В рамках этой тематики рассматриваются модели, основанные на булевых, многозначных, автоматных функциях, графовых структурах. Полученные результаты можно применять в таких приложениях, как обработка, хранение и сжатие данных, распознавание образов, защита информации, программирование.

В.Б. Алексеевым, А.А. Вороненко, С.С. Марченковым, А.С. Нагорным получены существенные результаты о строении решеток классов различных дискретных функций. В частности, найдено описание значимых фрагментов континуальных решеток этих классов. А.А. Сапоженко, А.А. Дайняком разрабатываются комбинаторный и графовый подходы к решению задач информатики. На основе этих подходов А.А. Сапоженко установлены принципиальные результаты о количествах комбинаторных объектов определенного вида. Среди них асимптотически точные оценки числа антицепей в унимодальных частично упорядоченных множествах, а также числа множеств, свободных от сумм. С.Н. Селезневой развивается алгебраический подход к задачам информатики с применением полиномиальных заданий дискретных функций. В рамках этого подхода получены оценки сложности задания дискретных функций в различных классах полиномиальных форм.

Проводимые исследования были поддержаны грантами Российского фонда фундаментальных исследований и Федеральной целевой программой «Научные и научно-педагогические кадры инновационной России».

Спецсеминары: Дискретная математика и математическая кибернетика, Дискретные функции и сложность алгоритмов, Дискретный анализ, Некоторые вопросы синтеза управляющих систем, Теория управляющих систем и математические модели СБИС, Сложность решения дискретных задач.

Теория синтеза, надежности и контроля дискретных управляющих систем, математические модели СБИС

(проф. С. А. Ложкин, проф. А. М. Марченко, доц. Д. С. Романов, асс. М.С.Шуплецов, м.н.с. Б.Р.Данилов)

На кафедре математической кибернетики изучаются различные вопросы теории синтеза, надёжности и контроля дискретных управляющих систем, исследуются возможности и способы применения научных результатов, полученных в данной области, при решении ряда задач проектирования современных сверхбольших интегральных схем (СБИС) и, в частности, СБИС наноуровня.

Значительная часть исследований по теории синтеза и сложности схем ведется в рамках традиционного для отечественной школы математической кибернетики асимптотического подхода, предложенного в работах К. Шеннона, О.Б.Лупанова, С.В.Яблонского. В этой области интенсивно развивается созданное С.А.Ложкиным новое направление, которое связано с разработкой методов синтеза, позволяющих получать асимптотические оценки высокой степени точности для сложности реализации «типичной» или самой «сложной» функции в различных классах систем. Указанные оценки установлены как для многих рассматривавшихся ранее моделей дискретных управляющих систем, так и для некоторых новых классов схем таких, например, как предикатные схемы (М.С.Шуплецов).

С.А.Ложкиным и его учениками получен также целый ряд результатов по исследованию сложности и структуры оптимальных схем для функций, встречающихся в приложениях (линейные функция, мультиплексорная функция и др.)

Как при реализации самых «сложных» функций, так и в области «индивидуального» синтеза изучаются различные модели "вложения" схем в те или иные "геометрические" структуры (плоские прямоугольные решетки, единичные кубы и др.), разрабатываются эффективные методы построения и оптимизации таких вложений. С.А.Ложкиным и его учениками получены, в частности, существенные результаты о сложности клеточных схем, которые являются «грубой» топологической моделью СБИС, о вложении двоичных и троичных деревьев в плоские прямоугольные решетки, о построении в единичных кубах с частично раскрашенными вершинами систем так называемых одноцветных связывающих поддеревьев и др.

Теория надежности и контроля схем являются важной и быстро развивающейся областью математической кибернетики. Д.С.Романов и его ученики ведут исследования в данной области, разрабатывают методы построения тестов различных типов, получают верхние и нижние оценки их длины. В результате этих исследований предложен, в частности, метод мультиразбиений, позволяюший получать "хорошие" тесты для блочных периодических контактных схем, созданы методы построения проверяющих и диагностических тестов для локальных кратных слипаний входов схемы и др.

Научно-исследовательская работа по математическим проблемам автоматизации синтеза СБИС проводится на кафедре под руководством А.М.Марченко, который является руководителем научно-исследовательского подразделения фирмы Нангейт — мирового лидера в области разработки средств автоматизированного проектирования библиотечных элементов нанометрового диапазона и официальным экспертом госкорпорации Роснано, с участием представителей ряда внешних организаций таких, как компаний Интел (www.intel.com), Нангейт (www.nangate.com) и др.

Проводимые исследования направлены на создание методов автоматизации проектирования топологии СБИС, синтеза библиотечных элементов, верификации схем и др. Основные задачи, которые необходимо при этом решать, относятся к классу NP-полных задач, то есть являются алгоритмически сложными. Для их решения используются разные методы теории алгоритмов, теории графов, вычислительной геометрии, линейного, нелинейного и целочисленного программирования.

С 2009 года на кафедре функционирует магистерская программа «Математические модели и методы проектирования СБИС» (http://master.cmc.msu.ru), которая предназначена для подготовки магистров в области математического и программного обеспечения систем автоматизации проектирования. Основными математическими разделами той части программы, которая определяет ее специализацию, являются: структурная теория схем, сложность комбинаторных алгоритмов, математические модели EDA, теория графов и комбинаторика, языки описания схем и проблемы верификации, теория надежности и контроля схем и др. Во время обучения по данной программе студенты овладевают также современными средствами автоматизации проектирования ведущих фирм (Cadence, Synopsis и др.), получают необходимые для практической работы навыки. При выполнении квалификационных работ студентам предоставляется возможность проходить практику в фирмах Интел и Нангейт.

Около 10 выпускников кафедры, которые специализировались в области теории управляющих систем и методов синтеза СБИС, работают в настоящее время в ряде фирм, связанных с проектированием СБИС (Интел – 1, Нангейт – 3, LSI Logic – 2, Cadance – 1 и др.).

Спецсеминары: Некоторые вопросы синтеза управляющих систем, Теория управляющих систем и математические модели СБИС.

Разработка математических моделей и методов верификации программ

(проф. В.А. Захаров, м.н.с. В.В.Подымов)

Одной из центральных задач математической кибернетики является задача анализа поведения сложных информационных систем (микроэлектронных схем, компьютерных программ, сетевых протоколов и др.). Для решения этой задачи применяются математические модели и методы теории автоматов и формальных языков, алгебры, математической логики, теории булевых функций. Разработанные модели и методы применяются, в частности, для решения задачи верификации программ – проверки того, что вычисления программы удовлетворяют заданным требованиям, предъявляемым к ее поведению. Сотрудники кафедры математической кибернетики внесли существенный вклад в исследование этой задачи. Для решения проблем эквивалентности и эквивалентных преобразований программ была разработана и развита теория алгебраических моделей программ, на основе которой были созданы эффективные алгоритмы проверки эквивалентности программ и полные системы эквивалентных преобразований программ. В тесном сотрудничестве с лабораторией вычислительных комплексов факультета ВМК и Институтом системного программирования РАН проводятся исследования в области обфускации (маскировки) программ, а также в области верификации распределенных программ и встроенных систем.

Проводимые исследования были поддержаны грантами Российского фонда фундаментальных исследований и Федеральной целевой программой «Научные и научно-педагогические кадры инновационной России».

Спецсеминар: Теоретические проблемы программирования.