Верификация программ на основе соотношений подобия

Описывается подход к статической верификации исполняемых программ на основе сопоставления семантических аспектов вычислений, позволяющий построить паспорт  программы. Паспорт, как результат статической верификации, может быть использован для создания среды контролируемого выполнения программ (динамической верификации реально выполняемых программ, прошедших статическую верификацию).