Альт-Эрго

Альт-Эрго
Разработчик(и)	OCamlPro
Репозиторий	github.com/OCamlPro/alt-ergo ;
Написано в	OCaml
Доступно в	Английский
Тип	Математический решатель, верификатор программ
Веб-сайт	alt-ergo.ocamlpro.com

SMT-решатель для проверки программного обеспечения

Alt-Ergo — автоматический решатель математических формул , в основном используемый при формальной проверке программ . Он работает по принципу выполнимости по модулю теорий (SMT). Разработка велась исследователями из Университета Париж-Юг , Лаборатории исследований в области информатики, Института исследований в области информатики (Inria Saclay Ile-de-France) и Национального исследовательского центра научных исследований (CNRS) . С 2013 года управление проектом и его контроль осуществляются компанией OCamlPro. ^[1] Он выпускается под свободной и открытой лицензией программного обеспечения CeCILL-C.

Технологии

Выбор дизайна

Alt-Ergo использует специализированный язык ввода с предварительным полиморфизмом , разработанный для сокращения числа аксиом, требующих квантификации, и упрощения сложности проблем. Хотя Alt-Ergo предлагает частичную поддержку языка SMT-LIB 2, его эффективность с файлами SMT сравнительно ограничена.

Основные компоненты

Основная архитектура Alt-Ergo состоит из трех основных элементов: решатель SAT на основе поиска в глубину (DFS) , механизм инстанцирования квантификаторов, использующий электронное сопоставление , и сборка процедур принятия решений для ряда встроенных теорий. Эти компоненты в совокупности обеспечивают возможности Alt-Ergo в автоматическом решении формул.

Встроенные теории

Alt-Ergo реализует процедуры (полу)принятия решений для следующих теорий:

Пустая теория.
Линейная целочисленная арифметика
Линейная рациональная арифметика
Нелинейная арифметика
Арифметика с плавающей точкой
Полиморфные массивы
Перечислимые типы данных
символы переменного тока
Типы данных записи

Промышленное использование

На базе Alt-Ergo построено несколько платформ проверки:

Why3, платформа для дедуктивной проверки программ, использует Alt-Ergo в качестве основного доказывающего средства ^[2]
CAVEAT, C-верификатор, разработанный CEA и используемый Airbus; Alt-Ergo был включен в квалификационный DO-178C одного из ее самолетов ^{[ необходима ссылка ]}
Frama-C , фреймворк для анализа C-кода, использует Alt-Ergo в плагинах Jessie и WP (предназначенных для дедуктивной проверки программ )
SPARK использует Alt-Ergo (позади GNATprove) для автоматизации проверки некоторых утверждений в Spark 2014
Atelier-B может использовать Alt-Ergo вместо своего основного средства проверки (увеличивая успешность с 84% до 98% в тестах проекта ANR Bware)
Rodin , фреймворк B-метода, разработанный Systerel, может использовать Alt-Ergo в качестве бэкэнда
Cubicle — программа проверки моделей с открытым исходным кодом для проверки свойств безопасности систем перехода на основе массивов
EasyCrypt, набор инструментов для рассуждений о реляционных свойствах вероятностных вычислений с использованием состязательного кода
БВАРЕ ^[3]
Кофеин ^[3]
FUI Hi-Lite ^[3]
Декерт ^[3]
ADT Альт-Эрго ^[3]
А3ПАТ ^[3]

Смотрите также

Ссылки

^ "О нас". alt-ergo.ocamlpro.com . Получено 15 июня 2023 г. .
^ "Why3". why3.lri.fr . Получено 15 июня 2023 г. .
^ abcdef "The Alt-Ergo Theorem Prover: Academic Web Page". alt-ergo.lri.fr . Получено 15 июня 2023 г. .

Внешние ссылки

Официальный сайт , OcamlPro
Alt-Ergo в LRI

Эта статья о научном программном обеспечении — заглушка . Вы можете помочь Википедии, расширив ее.

[1] "О нас". alt-ergo.ocamlpro.com . Получено 15 июня 2023 г. .

[2] "Why3". why3.lri.fr . Получено 15 июня 2023 г. .

[:0-3] "The Alt-Ergo Theorem Prover: Academic Web Page". alt-ergo.lri.fr . Получено 15 июня 2023 г. .