Ранее я описывал формальную верификацию на примере задачи о Волке, Козе, и капусте.
Ее решение и стало основой символьной виртуальной машины.

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

Символьные вычисления за один запуск дадут нам ответ, возможно ли получение нами нужного результата и пример набора таких входных параметров. Либо же доказательство того, что таких параметров нет.

Более того, мы можем задать входные аргументы вообще как все возможные, и выберем только выходной, например пароль администратора.
В этом случае мы найдём все уязвимости программы или же получим доказательство того, что пароль админа в безопасности.

Можно заметить, что классическое выполнение программы с конкретными входными данными представляет собой лишь частный случай символьного.
Поэтому наша символьная VM может работать и в режиме эмуляции стандартной виртуальной машины.
Читать дальше ->

https://habr.com/ru/post/450016/?utm_source=habrahabr&utm_medium=rss&utm_campaign=450016