Альт-Эрго - Википедия - Alt-Ergo

Альт-Эрго это автоматический решатель математических формул, специально разработанный для проверки программ. Он основан на выполнимость по модулю теорий (SMT). Он распространяется под лицензией с открытым исходным кодом (Cecill-C). Его первоначальными авторами были Сильвен Кончон и Эвелин Контеджан, в LRI, но сейчас он разрабатывается и поддерживается в OCamlPro.

Технологии

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

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

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

Ядро Alt-Ergo состоит из трех частей: решателя SAT на основе DFS, механизма создания экземпляров квантификаторов на основе E-Matching и комбинации процедур принятия решений для набора встроенных теорий.

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

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

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

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

  • Почему3 платформа для дедуктивной верификации программ использует Alt-Ergo в качестве основного средства проверки;
  • CAVEAT, C-верификатор, разработанный CEA и используемый Airbus; «Альт-Эрго» попал в квалификацию DO-178C одного из своих самолетов;
  • Фрама-С, фреймворк для анализа C-кода, использует Alt-Ergo в плагинах Jessie и WP (предназначенных для «дедуктивной проверки программ»);
  • ИСКРА, использует Alt-Ergo (за GNATprove) для автоматизации проверки некоторых утверждений в Spark 2014;
  • Ателье-Б может использовать Alt-Ergo вместо основного прувера (увеличение успеха с 84% до 98% на Тесты ANR Bware project );
  • Роден фреймворк B-методов, разработанный Systerel, может использовать Alt-Ergo в качестве бэкэнда;
  • Кабина, средство проверки моделей с открытым исходным кодом для проверки свойств безопасности систем перехода на основе массивов.
  • EasyCrypt, набор инструментов для рассуждения о реляционных свойствах вероятностных вычислений с состязательным кодом.

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

внешняя ссылка