axiom-symbolic

This content is not available in your language yet.

Это первый не bounded proof-backend Axiom. Он символически исполняет AXIOM-PROGRAM/2 в affine path states и доказывает одномерные quantifier-free linear-integer obligations через точную проверку целочисленной выполнимости их отрицания.

Фрагмент намеренно узкий. Неподдерживаемые инструкции и формулы отвергаются, а не приближаются. Внутри заявленного фрагмента конечный диапазон входов не перебирается.

python axiom_symbolic.py verify spec.aix program.axp \
  --proof program.axproof \
  --counterexample counterexample.axcex

Связанные исследования

Этот компонент входит в исследовательский проект Axiom. Все компоненты собраны по теме localzet-axiom. Основной язык документации — русский. Исследовательские результаты и ограничения не означают готовность к промышленному применению.

Исходный код · MIT