WikiDer > Альт-Эрго - Википедия
 | Эта статья содержит контент, который написан как Реклама. (Март 2015 г.) (Узнайте, как и когда удалить этот шаблон сообщения) |
 | Эта статья не цитировать любой источники. (Ноябрь 2014 г.) (Узнайте, как и когда удалить этот шаблон сообщения) |
Альт-Эрго это автоматический решатель математических формул, специально разработанный для проверки программ. Он основан на выполнимость по модулю теорий (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, набор инструментов для рассуждения о реляционных свойствах вероятностных вычислений с состязательным кодом.
Смотрите также
внешняя ссылка
 | Этот научное программное обеспечение статья - это заглушка. Вы можете помочь Википедии расширяя это. |