18.12.2025. VeHa-2025. Семинар ИНТЕЛЛЕКТУАЛЬНЫЕ СИСТЕМЫ и СИСТЕМНОЕ ПРОГРАММИРОВАНИЕ
Семинар ИНТЕЛЛЕКТУАЛЬНЫЕ СИСТЕМЫ и СИСТЕМНОЕ ПРОГРАММИ-РОВАНИЕ. Дата: 18.12.2025 Докладчики: Шилов Н.В., Кондратьев Д.А. и др. Тема: Об итогах соревнования по формальной верификации программ VeHa-2025 Аннотация Третье всероссийское соревнование по формальной верификации программ “VeHa-2025 — III Контест VeHa” прошло 4–8 ноября, оно стало мероприятием-спутником XXVI Открытой Всесибирской олимпиады по программированию им. И. В. Поттосина. В соревнованиях приняли участие команды из Новосибирского государственного университета, Группы Астра, Лаборатории Касперского, Института системного программирования им. В.П. Иванникова РАН, Математического института им. В. А. Стеклова РАН, Санкт-Петербургского политехнического университета Петра Великого, МГТУ им. Н. Э. Баумана, Университета Неаполис Пафос, Московского физико-технического института, Университета ИТМО, Университета МИСИС и Института автоматики и электрометрии СО РАН. На семинаре будет проведена церемония награждения лауреатов VeHa-2025 из Ново-сибирска. Кроме награждения состоятся короткие выступления (по 20 минут): (1) дипломантов VeHa-2025 по решенным задачам (*) Нейзов Максим Вячеславович (TLA+: Temporal Logic of Actions + data structures) – онлайн; (*) Черненко Иван Михайлович (Пошаговое выведение свойств в Isabelle/HOL); (*) Ищенко Артем Дмитриевич (Пошаговое выведение свойств в Isabelle/HOL). (2) Кондратьева Дмитрия Александровича - о номинации "Дедуктивная верификация решающей квадратичное диофантово уравнение Пелля программы, реализующей разработанный в Индии метод «чакравала», являющийся одним из первых в истории математики циклическим алгоритмом". - К сожалению, в выступлении Д.А. Кондратьева на слайде 15 (в записи на 37 мин 45 секунд, https://rutube.ru/video/f9f9ef521e8e57d03aae695af21494ab/?t=2265&r=plwd) допущена ошибка: на самом деле решение команды SPbPU-40202 является полным и правильным, не имеет опечаток и позволяет провести верификацию в автоматическом режиме. - Организаторы соревнования VeHa-2025 приносят извинения команде SPbPU-40202 за это ошибку с нашей стороны.
Семинар ИНТЕЛЛЕКТУАЛЬНЫЕ СИСТЕМЫ и СИСТЕМНОЕ ПРОГРАММИ-РОВАНИЕ. Дата: 18.12.2025 Докладчики: Шилов Н.В., Кондратьев Д.А. и др. Тема: Об итогах соревнования по формальной верификации программ VeHa-2025 Аннотация Третье всероссийское соревнование по формальной верификации программ “VeHa-2025 — III Контест VeHa” прошло 4–8 ноября, оно стало мероприятием-спутником XXVI Открытой Всесибирской олимпиады по программированию им. И. В. Поттосина. В соревнованиях приняли участие команды из Новосибирского государственного университета, Группы Астра, Лаборатории Касперского, Института системного программирования им. В.П. Иванникова РАН, Математического института им. В. А. Стеклова РАН, Санкт-Петербургского политехнического университета Петра Великого, МГТУ им. Н. Э. Баумана, Университета Неаполис Пафос, Московского физико-технического института, Университета ИТМО, Университета МИСИС и Института автоматики и электрометрии СО РАН. На семинаре будет проведена церемония награждения лауреатов VeHa-2025 из Ново-сибирска. Кроме награждения состоятся короткие выступления (по 20 минут): (1) дипломантов VeHa-2025 по решенным задачам (*) Нейзов Максим Вячеславович (TLA+: Temporal Logic of Actions + data structures) – онлайн; (*) Черненко Иван Михайлович (Пошаговое выведение свойств в Isabelle/HOL); (*) Ищенко Артем Дмитриевич (Пошаговое выведение свойств в Isabelle/HOL). (2) Кондратьева Дмитрия Александровича - о номинации "Дедуктивная верификация решающей квадратичное диофантово уравнение Пелля программы, реализующей разработанный в Индии метод «чакравала», являющийся одним из первых в истории математики циклическим алгоритмом". - К сожалению, в выступлении Д.А. Кондратьева на слайде 15 (в записи на 37 мин 45 секунд, https://rutube.ru/video/f9f9ef521e8e57d03aae695af21494ab/?t=2265&r=plwd) допущена ошибка: на самом деле решение команды SPbPU-40202 является полным и правильным, не имеет опечаток и позволяет провести верификацию в автоматическом режиме. - Организаторы соревнования VeHa-2025 приносят извинения команде SPbPU-40202 за это ошибку с нашей стороны.