応用プログラム解析ラボでは、開発者が日常のアクティビティにおいて直面する問題に対し、新しいプログラム解析手法の探索と既存の手法の採用を試みています。
一部の研究活動は JetBrains 内部のニーズに焦点を当てていますが、より一般的なケースを対象としたプロジェクトも実施しています。 また、Kotlin プログラミング言語の新機能の設計と実装なども行っています。
このプロジェクトでは、Kotlin コンパイラーのテストに対するファジングの応用を調査しています。 前回の研究では、コンパイラーに多数のバグを検出しました。 現在、さらに多くのコンパイラーコンポーネントにファジングプロセスを拡大し、コンパイラーの品質管理パイプラインに含められるように取り組んでいます。
Kex は当ラボの Java バイトコード解析プラットフォームです。Java バイトコードの読み込み、中間モデルの構築、および SMT ソルバーによるモデルの解析をサポートしています。 現時点では、Kex はテストの生成に焦点が当てられていますが、クラッシュの再現、プログラム解析、修復などにも使用することを検討しています。
このプロジェクトでは、自己整合性が LLM 生成コードの品質を評価する尺度として適しているかどうかを明らかにしようとしています。LLM は同じプロンプトが提示された場合には自己整合性の取れた結果を出し、指定された整合性の定義を満たす解決策を生成します。 このプロジェクトでは差動テストを使用して整合性を評価しています。つまり、生成されるすべての解決策が指定された、または生成されたテストスイートで同じように動作するかどうかを検証しています。 テストを生成するため、Kex をテスト生成モードで適用します。
LLM は異なる言語間の変換に適していると考えられています。 当ラボではこの考えが Gradle のビルド構成を .gradle
から .gradle.kts
に変換する際の問題にも当てはまるどうかを明らかにしようとしています。 これは、古い Groovy API から新しい Kotlin API を使用するように変換する場合に最も関係します。 当ラボでは IntelliJ プラットフォームのツールを使って Gradle からビルド構成を抽出する前後の要約を比較することで、評価を行っています。