Данная работа посвящена обзору методов решения актуальной на сегодняшний день задачи аспектно-ориентированного анализа эмоциональной окраски текстов. Данная задача решалась в рамках нескольких конференций, посвященных автоматическому анализу текстов на естественном языке. Организаторы конференций предлагали участникам площадки для сравнительного тестирования методов. В рамках данной работы рассмотрены методы решения задачи аспектно-ориентированного анализа эмоциональной окраски, предложенные участниками двух таких международных площадок: SemEval-2015 и SentiRuEval-2015.

Разработанная в ИСП РАН программная система Unihub является облачной вычислительной системой типа SaaS и предоставляет пользователям возможность удаленной работы через Web-браузер с интерактивными графическими Linux-приложениями, запускаемыми в изолированных Docker контейнерах. Контейнеры имеют динамические требования к вычислительным ресурсам. Обычный способ размещения, при котором контейнеры распределяются равномерно по всем имеющимся в распоряжении серверам, приводит к неравномерной загрузке системы: некоторые сервера перегружены, а некоторые простаивают. В данной работе мы предлагаем собирать данные о поведении пользователей и характере работы различных приложений с целью прогнозирования создаваемой контейнерами нагрузки. Наши наблюдения показывают, что полученная информация позволяет равномернее загрузить имеющееся в распоряжении оборудование и увеличить предельную производительность системы в целом.

В работе рассматривается задача создания виртуальных Apache Spark и Apache Hadoop кластеров для обработки больших данных в облачных средах. Проведен обзор существующих методов создания Apache Spark кластеров. Также описывается реализованный способ создания Apache Spark кластеров и сервиса для выполнения Apache Spark задач в среде OpenStack. Предложенное решение включено в проект OpenStack Sahara и доступно начиная с релиза OpenStack Liberty.

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

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

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

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

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

В статье рассматриваются методы тестирования компонентов ядра ОС Linux с использованием симуляции сбоев. Основная цель таких методов - проверка поведения модуля при возникновении нештатных ситуаций, таких как сбои в аппаратуре или нехватка ресурсов. Эти ситуации на практике встречаются достаточно редко и непредсказуемо, что существенно затрудняет их обнаружение и локализацию. Единственным распространённым подходом к поиску таких проблем является случайное внесение сбоев в ходе выполнения обычных тестов. В статье предлагаются новые методы систематического тестирования устойчивости к сбоям, а также приводятся результаты их апробации на реальных тестовых наборах в сравнении с уже использующимися методами.

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

Известно что если P≠NP то задача аппроксимации суммарной раскраски двудольных графов не может быть осуществлена в полиномиальное время с точностью для некоторой константы . Мы предлагаем для сколь угодно малого приближенный алгоритм для данной проблемы который работает за полиномиальное в среднем время.