УНИВЕРСИТЕТ ИТМО
Кафедра «Технологии программирования»

(версия для печати)




---



1. Меня зовут Вячеслав Миронов, я заканчиваю пятый курс специальности "Программное обеспечение вычислительной техники и автоматизированных систем" в Иркутском государственном университете путей сообщения. У меня большой опыт в работе с UNIX-системами: администрирование, программирование, но работа на предприятиях меня не интересует, я хотел бы попытаться сделать научную карьеру и соответственно хотел бы поступить в аспирантуру.

   Я ищу научного руководителя, у которого имеются интересные проблемы в области Computer Science.

   Я сейчас пишу диплом на тему использования графов для исследования исходных текстов программ (теория + программа). Выступал на всероссийской конференции Винеровские чтения-2009. Есть публикация, могу вам выслать, если заинтересуетесь. Также недавно в область моих интересов стал попадать раздел темпоральной логики (CTL, LTL). В общем, я совсем не против различных задачек в области Computer Science.

   Вячелав Миронов, viacheslav-mironov@yandex.ru

2. Мы занимаемся автоматным программированием (http://is.ifmo.ru/books/_book.pdf) во всем его многообразии, включая верификацию, где используются темпоральные логики. Посмотри сайт http://is.ifmo.ru/ и, в частности, http://is.ifmo.ru/verification/. В конце этой страницы четыре наших отчета по верификации. Есть и диссертации, которые у меня защищали http://is.ifmo.ru/disser/. Там есть многое из чего выбрать http://is.ifmo.ru/works/.

   С уважением, Шалыто

3. Добрый день, Анатолий Абрамович!

   Внимательно изучил Ваши ссылки. Прочитал про автоматное программирование. Очень понравились четыре отчета о верификации. Меня как раз интересует эта проблема, а литературы, описывающей инструменты нет. Ваши отчеты очень интересны в этом плане - расписывается все на реальных примерах. Ранее я никогда не сталкивался с проблемой верификации кода, разве что в университете писали свой лексический анализатор - некий интерпретатор собственного языка, но это отдаленно.

   Сейчас я активно прорабатываю данную область и понимаю, что тут много чего интересного. Особенно темпоральная логика LTL и CTL. Литературу в этой области найти сложно, поэтому собираю "с миру по нитке": посмотрел видеолекции Бориса Конева о верификации, читаю различные статьи с конференций, вот и ваш сайт тут является хорошим источником информации.

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

   Также почитал про SWITCH-технологию. Оказывается я с ней знаком, имею представление, но не знал, что она так называется. В целом, направление работ у вас очень интересное и, пожалуй, уникальное в стране. Возможно, ли подобрать тему аспирантской деятельности, связанную с верификацией программного обеспечения?

   С уважением, Вячеслав.