Оглавление
ACL2
-
Обзор ACL2
- ACL2 – это программная система для автоматизированных рассуждений в индуктивных логических теориях.
- Язык программирования ACL2 является прикладной версией Common Lisp без побочных эффектов.
- ACL2 является нетипизированным и тотальным языком, сопоставляющим каждый объект со своим аналогом.
- Базовая теория ACL2 аксиоматизирует семантику языка и его функций.
- Пользовательские определения расширяют теорию, сохраняя ее логическую последовательность.
-
Ядро программы и эффективность
- Ядро ACL2 для проверки теорем основано на переписывании терминов и является расширяемым.
- ACL2 построен на Common Lisp, что обеспечивает высокую эффективность и возможность компиляции.
-
Применение и награды
- ACL2 используется в промышленности для проверки теорем, включая доказательство корректности операции деления в микропроцессоре AMD K5.
- Среди промышленных пользователей ACL2 такие компании, как AMD, Arm, Centaur Technology и другие.
-
Дополнительные ресурсы
- Список помощников по проверке
- Рекомендации и внешние ссылки
- Веб-сайт ACL2 и интерфейс ACL2s на основе Eclipse для автоматизации и поддержки в доказательстве теорем.