リサーチグループ

検証またはプログラム分析ラボ

Verification or Program Analysis Lab（VorPAL）は、2015年、JetBrainsとサンクトペテルブルク工科大学コンピュータサイエンス技術研究所と共同して設立されました。

VorPALでは、学生、院生、および研究員らが、検証、静的解析、およびプログラム変換技法などの形式手法に基づき、ソフトウェアテクノロジーを開発しています。これらの手法は、スタンドアロンツール、プログラミング言語拡張、またはIDEプラグインとしての開発者の日常的な生産性を向上させるために使用されています。

オープンリサーチを心から信じている私たちの作業は、ほぼ常にオープンソースです。

現在のリサーチプロジェクト

Kotlin 改良計画

Kotlinは比較的新しいプログラミング言語です。ほかのプログラミング言語（Java）のいくつかの重要な問題と欠点を解決する言語ではありますが、同時に、改善と拡張の余地が未だ残っています。

VorPALでは、Kotlinを拡張するために、次の手法を模索済みまたは現在模索中です。

マクロ
Liquid型
パラメーター化されたクラス特殊化
Reifiedクラスのジェネリクス
Typeクラス
パターンマッチング
可変個引数ジェネリック

Kotlinのコンコリックテスト（KEX）

コンコリック（CONCrete + symbOLIC）テストは、ソフトウェアのテストと検証において興味深いハイブリッド手法で、静的と動的の両方のアプローチを組み合わせてプログラム解析を行います。私たちのKEXというプロジェクトでは、Kotlinにコンコリックテストを適用することを試みています。

Kotlinコンパイラーファジング（BBF）

ファジングとはよく知られたテスト手法で、コンパイラーテストに有効であることが実証されています。バックエンドバグファインダー（BBF）はファジング（および他の様々な興味深い手法）を使用して、Kotlinコンパイラ―に潜むバグを見つけ出します。

開発者生産性ツール

VorPALでは、Kotlinだけでなく、ソフトウェア開発に関わるすべての事柄に気を配っています。 Kotlinに直接関係のないプロジェクトには、JVMにおける条件ブレークポイントの高速化、AFLをシステム呼び出し対応にすること、およびGraalVMを介してクロス言語方式でツールを適用する試みがあります。