О журнале

Научный электронный журнал "Системная информатика" основан в 2013 году.

Учредитель - Федеральное государственное бюджетное учреждение науки Институт систем информатики им. А.П. Ершова Сибирского отделения Российской академии наук.

Свидетельство о государственной регистрации СМИ - ЭЛ № ФС 77-55164.

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

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

Читать дальше

Скачать

Описание системы: Russell — логический каркас для дедуктивных систем

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

Метод верификации параллельного и распределенного программного обеспечения на C# путем проведения трансформации абстрактного синтаксического дерева Roslyn в модель на Promela

В статье мы описываем подход для формальной проверки параллельных и распределенных программ на C#. Мы используем технологию Microsoft Roslyn для получения синтаксической и семантической информации об интересных конструкциях в реальном коде, чтобы сгенерировать соответствующий код на модельном языке Promela, предназначенном для описания взаимодействующих систем на основе акторов. Затем мы проверяем...
Скачать

Верификация предикатной программы бинарного поиска объекта произвольного типа

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