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

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

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

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

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

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