Внимательно изучил Ваши ссылки. Прочитал про автоматное программирование. Очень понравились четыре отчета о верификации. Меня как раз интересует эта проблема, а литературы, описывающей инструменты нет. Ваши отчеты очень интересны в этом плане - расписывается все на реальных примерах. Ранее я никогда не сталкивался с проблемой верификации кода, разве что в университете писали свой лексический анализатор - некий интерпретатор собственного языка, но это отдаленно.
Сейчас я активно прорабатываю данную область и понимаю, что тут много чего интересного. Особенно темпоральная логика LTL и CTL. Литературу в этой области найти сложно, поэтому собираю "с миру по нитке": посмотрел видеолекции Бориса Конева о верификации, читаю различные статьи с конференций, вот и ваш сайт тут является хорошим источником информации.
В своем дипломе я пишу специализированное кросс-платформенное средство, которое разбирает исходные тексты и строит графы. Таких средств очень мало, отличительная черта моего средства - модульность: модуль графического интерфейса, ядро, к ядру организовано динамическое подключение модулей для разбора соответствующих языков и удобный выбор исследуемой информации. Это не "академический" проект, этим средством вполне можно исследовать компоненты модуля ядра Линукс (например драйверы). Хочу сказать, что какие-то наработки в анализе исходных текстов имеются: сейчас закончен основной модуль для Си, к защите диплома для примера расширяемости добавлю модуль для анализа исходных текстов на втором языке.
Также почитал про SWITCH-технологию. Оказывается я с ней знаком, имею представление, но не знал, что она так называется. В целом, направление работ у вас очень интересное и, пожалуй, уникальное в стране. Возможно, ли подобрать тему аспирантской деятельности, связанную с верификацией программного обеспечения?
С уважением, Вячеслав.