Без заголовка

Не совсем. При верификации, генерируются так называемые VC - verification conditions. Т.е. теоремы которые нужно доказать, и если все теоремы верны, значит прога соответствует спецификации. Условно говоря, каждый путь в программе преобразуется в набор конъюнкций, где каждая конъюнкт ограничивает множество возможных значений переменных. В частности, там кодируются массивы и всякие вспомогательные конструкции. Вобщем получается много мусора, в котором трудно разобраться. Но из этого мусора, можно сделать обратную трансляцию, что-то типа стэк-трейса, только значения переменных задавать символически - в виде ограничений на их значения.