Альт-Эрго

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

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

Технологии

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

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

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

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

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

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

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

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

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

Why3 , платформа для дедуктивной проверки программ, использует Alt-Ergo в качестве основного средства проверки. ^[2]
CAVEAT, C-верификатор, разработанный CEA и используемый Airbus; «Альт-Эрго» вошел в квалификацию ДО-178С одного из своих самолетов. ^{[ нужна ссылка ]}
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]
ФУИ Привет-Лайт ^[3]
Десерт ^[3]
ADT Альт-Эрго ^[3]
А3ПАТ ^[3]