検証またはプログラム分析ラボ
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を介してクロス言語方式でツールを適用する試みがあります。
過去のリサーチプロジェクト
有界モデル検証
Cプログラミング言語向けに有界モデル検証ツールを作成しました。 LLVMツールチェーンと様々なSMTソルバーに基づくツールです。 時間とリソース不足により、このプロジェクトは 中断されています。
IDEのクローン検出
最新のアプローチを使って、効率的なオンラインクローン検出ツールの実装に成功し、リアルタイムで大規模なコードベースを解析できるようになりました。 数々の再考察を重ね、多大な努力を尽くした末、このツールは現在、IntelliJ IDEAのクローン検出機能として使用されています。
メインプロジェクト:
従来の並行プログラミングには、共有ミュータブルステートの操作が必要です。 弊社のリサーチ分野に興味のある学生の方は、詳細について、ラボ責任者であるVladimir Itsykson(vlad@icc.spbstu.ru)までぜひご連絡ください。
グループメンバー







