Извините. Я конечно невнятно излагаю. Вобщем есть некий более-менее формально описанный язык "C". Можно считать что язык этот вычислительно эквивалентен некоторому классу конечных автоматов - классу автоматов с числом состояний меньше некоторой константы, вроде той, что была в предыдущем комментарии. "Можно считать", но нельзя "доказать" потому что язык не до конца формализован. Но мы вроде согласились что стандарт описывает конечные автоматы.

Конечный автомат всегда либо останавливается за конечное число шагов либо повторяет уже бывшее состояние и тогда не остановится никогда. Отсюда легко понять, что для класса конечных автоматов с числом состояний менее данной константы можно сделать универсальный конечный автомат который их будет верифицировать. Верифицировать в том смысле что он будет говорить остановится ли данный конечный автомат и если да то в каком состоянии. Это был ответ на исходный вопрос можно ли программы верифицировать конечными автоматами: программы на C можно.

Далее возник обратный вопрос. Можно ли проверить программой на C т.е. конечным автоматом парность скобок. Ответ вроде бы очевиден - нет. "Вообразить" бесконечно большую виртуальную память нельзя в том смысле, что это будет не расширением языка "С", а противоречивой системой. В C все типы включая указатели имеют только конечное количество значений. На этом построен весь язык начиная от массивов.