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

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

Процесс-ориентированное программирование является парадигмой, основанной на понятии процесса, где каждый процесс внутри является параллельным автоматом. Парадигма предназначена для разработчиков ПЛК (программируемых логических контроллеров) чтобы писать программное обеспечение для Industry 4.0. Язык poST - перспективное процесс-ориентированное расширение языка структурированного текста (ST) стандарта IEC 61131-3, обеспечивающее концептуальную согласованность исходного кода ПЛК с...

SSA-форма – промежуточное представление для компиляции императивных программ, где каждой переменной значение присваивается лишь единожды. Будучи правильно определённой, SSA-форма порождает семейство чисто синтаксических категорий с несколькими хорошими свойствами. Мы надеемся, что эта работа послужит основанием для категорного подхода к оптимизации.

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

В статье представлена текущая реализация языкового сервера для интерактивного доказателя теорем Rzk. Она анализирует соответствующие технологии, связанные с языковым сервером Protocol, расширениями VS Code и доказателями теорем, и как на их основе строится языковая поддержка для Rzk.