リサーチグループ

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

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

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

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

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

Better Kotlin

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

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

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

Kotlinのコンコリックテスト(KEX)

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

Kotlinコンパイラーファジング(BBF)

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

開発者生産性ツール

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

過去のリサーチプロジェクト

有界モデル検証

Cプログラミング言語向けに有界モデル検証ツールを作成しました。LLVMツールチェーンと様々なSMTソルバーに基づくツールです。時間とリソース不足により、このプロジェクトは 中断されています。

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
学生