Исследовательская группа

Лаборатория верификации и анализа программ

Научно-исследовательская лаборатория верификации и анализа программ создана в 2015 году компанией JetBrains и Институтом компьютерных наук и технологий Санкт-Петербургского политехнического университета Петра Великого. В ней студенты, аспиранты и молодые исследователи изучают технологии разработки программного обеспечения на основе формальных методов с применением верификации, статического анализа и трансформации программ.

В настоящее время в лаборатории ведутся четыре высокотехнологичных проекта.

Верификация программ и обнаружение ошибок на основе Bounded Model Checking. Цель проекта — создать инструменты, которые улучшают качество ПО, находя в нем ошибки и нарушения контрактов с помощью ограниченной проверки моделей и SMT-решателей.

Поиск клонов в программном коде. Интерактивный инструмент, разрабатываемый в лаборатории, интегрируется в среду разработки IntelliJ IDEA и на лету находит клоны.

Автоматизация исправления ошибок. В рамках этого направления создается инструмент, который автоматически исправляет часть программных ошибок, найденных средствами статического анализа.

Co-design на основе Kotlin. На базе языка программирования, созданного в JetBrains, в лаборатории разрабатывается технология co-design (совместного проектирования ПО и оборудования). Она использует объектно-ориентированные возможности Kotlin и призвана стать альтернативой существующим подходам, основанным на тяжеловесном и неповоротливом языке SystemC.

Студенты, заинтересованные в повышении своей квалификации в этих и смежных областях, могут обращаться к руководителю лаборатории Владимиру Михайловичу Ицыксону — vlad@icc.spbstu.ru

Новости