Научный сотрудник лаборатории Теоретического программирования ИСИ СО РАН
Научный сотрудник лаборатории Теоретического программирования ИСИ СО РАН к.ф.-м.н. Дмитрий Кондратьев награжден заведующим лабораторией YADRO НГУ благодарностью за успешную организацию и проведение Летнего Системного Буткемпа лаборатории YADRO НГУ. На Летнем Системном Буткемпе лаборатории YADRO НГУ Дмитрий курировал проект по дедуктивной верификации оптимизированных реализаций умножения матриц, установив на данном проекте работоспособность на практике наработанных в ИСИ СО РАН идей по упрощению дедуктивной верификации программ. – Необходимость дедуктивной верификации понятна уже десятилетиями. Однако на практике она очень сложна. Поэтому дедуктивная верификация долго не выходила из научных лабораторий и с трудом проникала в практику. И лишь в последнее время появились методы автоматизации, которые позволяют применять ее к практическим задачам.В этом проекте было очень важно понять, смогут ли студенты за довольно короткий промежуток времени освоить эффективную верификацию и применить ее к реальной программе реализации умножения матрицы. Я считаю очень положительным результатом проекта то, что участники, имея небольшую подготовку, изучили такую сложную область за две недели и при этом полностью успешно завершили верификацию реальной программы умножения матриц, – рассказал куратор проекта Дмитрий Кондратьев. Подробности о Летнем Системном Буткемпе лаборатории YADRO НГУ можно посмотреть в следующей новости НГУ: https://www.nsu.ru/n/media/news/obrazovanie/v-ngu-zavershilsya-letniy-sistemnyy-butkemp-laboratorii-yadro/#_r9e8u5jg1