연구 그룹

검증 또는 프로그램 분석 연구소

검증 또는 프로그램 분석 연구소(이하 VorPAL)는 JetBrains와 상트페테르부르크 폴리테크닉 대학의 컴퓨터 과학 및 기술 연구소가 2015년에 공동 설립했습니다.

VorPAL의 학생, 대학원생, 연구원은 검증, 정적 분석, 프로그램 변환 기술 같은 정형 기법을 기반으로 소프트웨어 기술을 개발하고 있습니다. 이러한 방법은 독립실행형 도구, 프로그래밍 언어 확장 프로그램, IDE 플러그인으로서 개발자의 일상적 생산성을 향상하는 데 사용됩니다.

본 연구소는 열린 연구의 힘을 깊이 신뢰하기에 작업을 거의 항상 오픈 소스로 공개합니다.

현재 연구 프로젝트

Kotlin 개선

Kotlin은 상대적으로 새로운 프로그래밍 언어로서, 다른 프로그래밍 언어(Java) 몇가지 중요한 문제와 단점을 해결합니다. 그러나 동시에 개선하고 확장할 수 있는 여지도 많습니다.

VorPAL에서는 Kotlin을 확장할 수 있는 다음과 같은 방법을 모색해왔습니다.

  • 매크로
  • Liquid 유형
  • 매개변수화된 클래스 분화
  • Reified 클래스 제네릭
  • 유형 클래스
  • 패턴 일치
  • Variadic 제네릭

Kotlin Concolic 테스트(KEX)

Concolic(CONCrete + symbOLIC) 테스트는 소프트웨어 테스트 및 검증을 위한 흥미로운 하이브리드 기술이며, 프로그램 분석에 대한 정적 및 동적 접근방식을 결합합니다. KEX라는 이름의 이 프로젝트에서는 Kotlin에 Concolic 테스트를 적용하려고 합니다.

Kotlin 컴파일러 퍼징(BBF)

퍼징(Fuzzing)은 컴파일러 테스트에서 효율성을 입증받은 잘 알려진 테스트 기법입니다. Backend Bug Finder(BBF)는 Kotlin 컴파일러에서 사소한 버그를 찾기 위해 퍼징(및 기타 수많은 흥미로운 기법)을 사용합니다.

개발자 생산성 도구

VorPAL에서는 Kotlin뿐만 아니라 소프트웨어 개발과 관련된 모든 것을 다룹니다. Kotlin 외 프로젝트로는 JVM의 조건부 중단점 가속화, AFL이 시스템 호출을 인식하도록 만들기, GraalVM을 통해 교차 언어 방식으로 도구 적용 등이 포함됩니다.

이전 연구 프로젝트

경계 모델 검사

LLVM 툴체인 및 다양한 SMT 솔버를 기반으로 Borealis라는 C 프로그래밍 언어용 경계 모델 검사 도구를 만들었습니다. 이 프로젝트는 시간과 리소스의 부족으로 중단 중입니다.

IDE에 대한 복제 탐지

최첨단 접근방식을 이용해 대규모 코드베이스를 실시간으로 분석할 수 있는 효율적인 온라인 복제 탐지 도구를 성공적으로 구축했습니다. 수차례의 반복과 많은 노력 끝에 이 도구는 IntelliJ IDEA로 이전되어 현재 복제 탐지에 사용되고 있습니다.

학생 인턴십

연중 상시 인턴을 채용합니다. 본 연구소의 연구 분야에 관심 있는 학생은 연구소장 Vladimir Itsykson(vlad@icc.spbstu.ru)에게 언제든지 문의하여 자세한 내용을 알아보세요.

그룹 멤버

Vladimir Itsykson
Vladimir Itsykson
프로젝트 관리자
Valentyn Sobol
Valentyn Sobol
연구원
Azat Abdullin
Azat Abdullin
연구원
Daniil Stepanov
Daniil Stepanov
연구원
Artyom Aleksyuk
Artyom Aleksyuk
연구원
Marat Akhin
Marat Akhin
연구원
Mikhail Belyaev
Mikhail Belyaev
연구원
Stanislav Ruban
Stanislav Ruban
학생