ACL2
-
Обзор ACL2
- ACL2 — это программная система для автоматизированных рассуждений в индуктивных логических теориях.
- Язык программирования ACL2 является прикладной версией Common Lisp без побочных эффектов.
- ACL2 нетипизирован и все функции являются тотальными.
- Базовая теория ACL2 аксиоматизирует семантику языка и его функций.
- Пользовательские определения расширяют теорию, сохраняя логическую последовательность.
-
Ядро программы и расширение
- Ядро ACL2 для проверки теорем основано на переписывании терминов и является расширяемым.
- ACL2 является «промышленной» версией NQTHM, средства доказательства теоремы Бойера-Мура.
- ACL2 повышает эффективность благодаря использованию Common Lisp, что позволяет компилировать и запускать спецификации.
-
Применения и награды
- ACL2 нашел множество применений в промышленности, включая доказательство корректности операций с плавающей запятой.
- Промышленными пользователями ACL2 являются AMD, Arm, Centaur Technology и другие.
- ACL2 получил награду ACM Software System Award за новаторство в 2005 году.
-
Дополнительные ресурсы
- Список помощников по проверке
- Рекомендации и внешние ссылки
- Веб-сайт ACL2 и ACL2s — интерфейс на основе Eclipse с расширенными функциями автоматизации.