KeYmaeraX -- это доказательство теорем в стиле Хоара для гибридных систем. Гибридную систему можно рассматривать как совокупность дискретных, так и непрерывных переменных, значения которых могут изменяться резко или непрерывно соответственно. KeYmaeraX поддерживает только переменные, имеющие примитивный тип bool или real. Благодаря сочетанию дискретных и непрерывных элементов системы, одной из перспективных областей применения KeYmaeraX являются системы управления с замкнутым контуром. Система управления с замкнутым контуром состоит из установки и контроллера. В то время как установка в основном представляет собой совокупность непрерывных переменных, значения которых меняются со временем в соответствии с физическими законами, контроллер можно рассматривать как алгоритм, сформулированный на классическом языке программирования. В этой статье мы рассмотрим некоторые недавние расширения исчисления доказательств, применяемые KeY\\-maeraX, которые делают формальные доказательства устойчивости динамических систем более выполнимыми. Основываясь на примере, мы сначала познакомимся с темой и докажем асимптотическую устойчивость данной системы.

В этой статье представлен новый подход к автонастройке программ, параллельных по данным. Автонастройка -- это поиск оптимальных параметров настройки программы, при которых её производительность оказывается максимальной. Новизна подхода состоит в использовании метода проверки моделей для поиска оптимальных параметров настройки методом контрпримеров. В нашей работе мы абстрагируемся от конкретных программ и конкретных процессоров, задавая их представительные абстрактные шаблоны. Наш метод контрпримеров состоит в реализации следующих четырёх шагов. На первом шаге на языке инструмента проверки моделей задаётся модель исполнения абстрактной программы на абстрактном процессоре. На втором шаге на языке инструмента проверки моделей формулируем свойство оптимальности, зависящее от построенной модели. На третьем шаге подбираем оптимальные значения параметров настройки посредством использования контрпримеров, построенных в ходе верификации свойства оптимальности. На четвёртом шаге извлекаем информацию о параметрах настройки из контрпримера для оптимальных параметров. Мы применяем этот подход к автонастройке параллельных программ, написанных на языке OpenCL -- современном популярном языке, который расширяет язык C для программирования как обычных многоядерных процессоров (CPU), так и массивно-параллельных графических процессоров (GPU). В качестве инструмента верификации мы используем верификатор SPIN и его язык представления моделей Promela, формальная семантика которого позволяет моделировать исполнение параллельных программ на процессорах с различной архитектурой.

К последовательным реагирующим системам относятся компьютерные программы и вычислительные устройства, которые обрабатывают потоки входных данных или сигналов управления и генерируют на выходе последовательности команд или результатов вычислений. Для проектирования таких систем полезно иметь формальные языки спецификаций, способные выражать отношения между входными и выходными потоками данных. В предшествующих работах нами было предложено семейство таких языков спецификаций, представляющих собой расширение темпоральных логик $LTL$, $CTL$ и $CTL^*$ за счет использования регулярных языков в качестве параметров темпоральных операторов. Мы провели сравнительный анализ выразительных возможностей нового расширения темпоральной логики линейного времени $Reg$-$LTL$ и предложили алгоритмы верификации моделей для новых расширений логик $Reg$-$LTL$, $Reg$-$CTL$, и $Reg$-$CTL^*$. Однако вопрос о сложности задач верификации моделей и проверки выполнимости формул указанных логик оставался открытым. В этой статье мы восполняем этот пробел в наших исследованиях и показываем, что для темпоральной логики $Reg$-$LTL$ обе задачи являются Pspace-полными. Вычислительная трудность рассматриваемых задач легко доказывается сведением к ним проблемы пустоты пересечения семейств регулярных языков. Основным результатом статьи является алгоритм сведения задачи проверки выполнимости формул логики $Reg$-$LTL$ к проблеме пустоты автоматов Бюхи сравнительно небольшого размера и описание стратегии, позволяющей проверять пустоту полученных автоматов с использованием объема памяти, полиномального относительно размера исходных формул.

В Институте систем информатики СО РАН разрабатывается система C-lightVer для дедуктивной верификации C-программ. C-kernel является промежуточным языком верификации в данной системе. Система облачного параллельного программирования (CPPS) также разрабатывается в Институте систем информатики СО РАН. Cloud Sisal является входным языком системы CPPS. Главной особенностью системы CPPS является неявное параллельное исполнение, основанное на автоматическом распараллеливании циклов Cloud Sisal. Cloud-Sisal-kernel является промежуточным языком верификации в системе CPPS. Нашей целью является автоматическое распараллеливание такого надмножества языка C, которое позволяет реализовать автоматическую верификацию. Нашим решением является такое надмножество языка C-kernel, как язык C-Sisal-kernel. Первым результатом, представленным в данной статье, является расширение языка C-kernel циклами языка Cloud-Sisal-kernel. В результате был разработан язык C-Sisal-kernel. Вторым результатом, представленным в данной статье, является расширение аксиоматической семантики языка C-kernel правилом вывода для циклов языка Cloud-Sisal-kernel. В данной статье также представлен наш подход к проблеме автоматизации дедуктивной верификации в случае финитных итераций над структурами данных. Такие циклы называются финитными итерациями. Нашим решением является композиция символического метода верификации финитных итераций, метагенерации условий корректности и смешанной аксиоматической семантики. Символический метод верификации финитных итераций позволяет задавать правила вывода для таких циклов без инвариантов. Символическая замена финитных итераций рекурсивными функциями является основой данного метода. Полученные условия корректности с применениями рекурсивных функций соответствуют логической основе системы доказательства ACL2. Мы используем систему ACL2, основанную на вычислимых рекурсивных функциях. Метагенерация условий корректности позволяет упростить реализацию новых правил вывода в системе верификации. Использование смешанной аксиоматической семантики приводит в некоторых случаях к более простым условиям корректности.

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

Мы представляем табличную процедуру, которая проверяет логические отношения между рекурсивно определенными подтипами рекурсивно определенных типов, и применяем эту процедуру к проблеме разрешения неоднозначных имен в языке программирования. Эта работа является частью проекта по разработке нового языка программирования, подходящего для эффективной реализации логики. Логические формулы представляют собой древовидные структуры со множеством конструкторов, имеющих различные свойства и типы аргументов. Алгоритмы, использующие эти структуры, должны выполнять анализ вариантов для конструкторов и получать доступ к поддеревьям, тип и существование которых зависят от используемого конструктора. Во многих языках программирования анализ прецедентов обрабатывается путем сопоставления, но мы хотим использовать другой подход, основанный на рекурсивно определенных подтипах. Вместо сопоставления дерева с различными конструкторами мы будем классифицировать его с помощью набора непересекающихся подтипов. Подтипы являются более общими, чем структурные формы, основанные на конструкторах, мы ожидаем, что они могут быть реализованы более эффективно и, кроме того, могут использоваться при статической проверке типов. Это позволяет использовать рекурсивно определенные подтипы в качестве предварительных условий или постусловий функций. Мы определяем типы и подтипы (которые мы будем называть прилагательными), определяем их семантику и даем проверку включения прилагательных на основе таблиц. Мы показываем, как использовать эту проверку включения для разрешения неоднозначных ссылок на поля в объявлениях прилагательных. Та же процедура может быть использована для разрешения неоднозначных вызовов функций.

В статье рассматривается способ решения задачи линейного программирования (ЗЛП), которая требует найти минимум или максимум линейного функционала на множестве неотрицательных решений системы линейных алгебраических уравнений с теми же неизвестными. Способ получен при усовершенствовании классического симплекс-метода, который, привлекая геометрические соображения фактически обобщает метод полных исключений Гаусса решения систем уравнений. Предлагаемый способ, как и метод полных исключений, исходит из чисто алгебраических соображений. Он заключается в преобразовании всей ЗЛП, включая целевую функцию, в эквивалентную задачу с очевидным ответом. Ради удобства преобразования целевого функционала, уравнения записываются как линейные функционалы в левой части и нули в правой. Из коэффициентов упомянутых функционалов составляется матрица, которая называется матрицей ЗЛП. Нулевая строка матрицы -- коэффициенты целевого функционала, $a_{00}$ -- его свободный член. Описание и обоснование алгоритмов ведется в терминах преобразования этой матрицы. При вычислениях матрица является расчетной таблицей. Рассматриваемый метод, по аналогии с симплекс-методом, состоит из трех этапов. На первом этапе матрица ЗЛП приводится к специальному 1-каноническому виду. При таких матрицах одно из базисных решений системы очевидно, и на нем целевой функционал равен $a_{00}$, что очень удобно. На втором этапе полученная матрица преобразуется в аналогичную матрицу с неположительными элементами нулевого столбца (кроме $a_{00}$), что влечет неотрицательность базисного решения. На третьем этапе матрица преобразуется в матрицу, обеспечивающую неотрицательность и оптимальность базисного решения. Для второго этапа, аналог которого в симплекс-методе использует искусственный базис и является наиболее трудоемким, приводятся два варианта без искусственных переменных. При описании первого из них, попутно, получен очень простой для понимания и запоминания аналог знаменитой леммы Фаркаша. Другой вариант совсем прост в применении, но его полное обоснование сложно и будет опубликовано отдельно.

Большой интерес вызывают исследования в области эффективных алгоритмов оценивания частоты. Причиной этому является перераспределение во многих современных радиотехнических приложениях роли аддитивного и фазового шумов. Примером может служить область измерительных радиоприборов, работающих, как правило, при высоких отношениях сигнал/шум (ОСШ). Ошибка оценки в большей степени определяется не широкополосным шумом, а частотными и фазовыми шумами гетеродинов приемных и передающих устройств. В частности, в более ранних работах [1] предложен эффективный вычислительный алгоритм оценивания частоты квазигармонического сигнала, основанный на итерационном вычислении АКП. В [2] этот алгоритм доработан и показана его близость к границе Рао-Крамера (источниками этих шумов являются задающие генераторы и синтезаторы частоты). Возможности оценивания частоты в радиоканалах позволяют существенно расширить функционал всей радиосети. Сюда можно отнести, например, задачу адаптивного распределения информационных потоков радиосети. Сюда же можно отнести задачи синхронизации и когерентной обработки сигналов. По этим причинам необходимы дополнительные исследования этого алгоритма, расчет теоретических границ и их сравнение с результатами моделирования.