Observations

Не понял что и как применить. Просто C как он описан в стандарте вопреки распространенному мнению не Turing complete. Программы на C можно верифицировать конечным автоматом. Можно разумеется и стековым. То же самое рассуждение применимо к более широкому классу языков.

Верификация программного обсепечения, неизвестная panchul, применяется военными и людьми занимающимися real-time. Есть периодическая конференция про это с proceedings на много сотен страниц. Spin и promela которые наверху упоминались вещи достаточно старые, они скорее про верификацию алгоритмов. Сейчас люди умеют верифицировать pointer arithmetics в многопоточных приложениях (Smallfoot, separation logic).