Add cit ru

Author: imustafin

_includes/refs/experience-at-cit.md

@@ -13,3 +13,4 @@
 [llm]: https://se.constructor.ch/publications/do-ai-models-help-produce-verified-fixes
 [llm-blog]: https://se.constructor.ch/2025/07/25/ai-models-verified-bug-fixes
 [feed]: {% link feed.xml %}
+[feed]: {% link ru/feed.xml %}

ru/_posts/2025-09-05-учёба-в-cit.md

@@ -0,0 +1,69 @@
+---
+layout: post
+title: Моя учёба в CIT
+ref: experience-at-cit
+---
+{% include refs/experience-at-cit.md %}
+Constructor Institute of Technology (CIT) — это
+институт в Шаффхаузене, Швейцария, в котором я
+провёл два года моей аспирантуры в области верификации программного
+обеспечения на Эйфеле. К сожалению, [СIT было решено закрыть в 2025][close].
+В этом посте я хочу сохранить ссылки на некоторые проекты,
+над которыми мы работали.
+
+Я работал на [кафедре программной инженерии][se]
+под руководством [Бертрана Мейера][bm]. В моё время
+на кафедре было ещё несколько аспирантов: [Ли Хуан][lh]
+(успела защититься и получила степень, поздравляю!),
+[Алессандро Скена][as] и [Рето Вебер][rw]. Нашу научную и преподавательскую
+деятельность поддерживал [Марко Пиччони][mp].
+
+## Статическая верификация в AutoProof
+Наша работа охватывала различные области программной инженерии.
+Особое внимание уделялось статической верификации. Главным продуктом
+команды в этой сфере является [AutoProof][autoproof],
+который является частью научного окружения [Reif][reif].
+AutoProof — это статический верификатор для программ на Эйфеле.
+С его помощью можно автоматически проверить согласуется ли
+тело процедуры с контрактами.
+
+Основная часть моего вклада в код верификатора заключается
+в реализации и расширении подхода, описанного в статье нашей кафедры
+["The concept of class invariant in object-oriented programming"][inv].
+К сожалению, наша работа была прервана закрытием института.
+
+## Могут ли LLM помочь с исправлением верифицированного ПО?
+Наше последнее исследование в институте изучало насколько
+чаты с LLM могут помочь в исправлении багов, когда у программистов
+есть доступ к верификтору. Отчёт об этом исследовании называется
+["Do AI models help produce verified bug fixes?"][llm].
+
+Я считаю, что верификация ПО может взять
+случайность в ответах больших языковых моделей под контроль. Верификатор
+может подтвердить, что исправление в самом деле "корректно", а не просто
+"статистически выглядит подходящим".
+
+Мы попросили 25 программистов исправить баги в программах.
+Некоторым был доступен чат-бот и верификатор, некоторым было разрешено
+работать только с верификатором.
+
+Результаты показали, что LLM наиболее полезны начинающим пользователям
+(чтобы добиться хоть какого-то результата) и экспертам (быстро реализовать
+самостоятельно придуманное решение). Разработчики со средним уровнем знаний
+получают меньше пользы от LLM.
+
+Я [писал больше][llm-blog] об эксперименте в блоге кафедры. Конечно,
+в самой статье можно получить ещё больше информации.
+
+## Планы на будущее
+У меня есть ещё несколько проектов из Constructor Institute of Technology,
+которые я бы хотел подсветить, но я оставлю их для будущих постов.
+Подпишитесь на [RSS ленту][feed], чтобы их не пропустить!
+
+В общем, я рад, что у меня была возможность для работы над продвинутыми
+темами программной инженерии в умелой команде, возглавляемой Бертраном Мейером.
+Условия работы были великолепными и позволили нам сконцентрироваться на
+науке. Лично мне грустно, что наша работа прервалась так резко.
+
+Я надеюсь, что у нас ещё будет возможность собраться командой и
+продолжить нашу работу.