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