Верификатор автоматический
Верификатор автоматический (Mechanical verifier) — схема обеспечения автоматического доказательства правильности программ. Включает генератор условий верификаций и блок доказательства теорем. [Домарева В.В. «Безопасность информационных технологий. Системный подход» —