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

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

Область исследований связана с технологиями создания высококачественного программного обеспечения на основе формальных методов с использованием верификации, статического анализа и технологий трансформации.

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

  • Разработка инструментов верификации программ и обнаружения ошибок на основе Bounded Model Checking. Цель проекта – повышение качества программного обеспечения путем обнаружения ошибок и нарушений контрактов с помощью методов ограниченной проверки моделей (BMC) и активного использования SMT-солверов.
  • Обнаружение клонов в программном обеспечении. Цель проекта – разработка интерактивного инструмента обнаружения клонов программного кода, интегрированного в среду разработки IntelliJ IDEA, и осуществляющего поиск клонов ”на лету”.
  • Автоматизированное исправление программных ошибок. Цель проекта – разработка инструмента, автоматически исправляющего часть программных ошибок, найденных средствами статического анализа.
  • Технология co-design на основе языка Kotlin Цель проекта – на базе современного языка программирования Kotlin, разрабатываемого в JetBrains, спроектировать технологию для совместного создания программного обеспечения и аппаратуры (co-design), использующую объектно-ориентированные возможности Kotlin, и способной стать альтернативой существующих подходов, основанных на тяжеловесном и неповоротливом языке SystemC.

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