C*: C言語におけるプログラミングと検証の統合

システムソフトウェアの正確な機能性を保証することは、その安全性と低レベルの性質から、形式検証の研究と応用の主要な焦点となっています。検証ツールの進歩にもかかわらず、従来のプログラマーは自身のコードの検証にほとんど関与しておらず、検証済みソフトウェアの開発および保守コストが高くなっています。検証プラクティスへのプログラマーの参加を妨げる主な障壁は、プログラミングと検証の実践との間の環境とパラダイムの断絶であり、これがアクセシビリティとリアルタイム検証を制限しています。 私たちはC*、C言語プログラミングのための証明統合型言語設計を紹介します。C*は、シンボリック実行エンジンとLCFスタイルの証明カーネルによって強化された検証機能でCを拡張します。これにより、プログラマーは実装コードの隣に証明コードブロックを埋め込むことができ、現在の証明状態のインタラクティブな更新を容易にすることで、リアルタイム検証を可能にします。その表現力豊かで拡張可能な証明サポートにより、ユーザーは論理定義、定理、およびプログラム可能な証明自動化の再利用可能なライブラリを構築できます。特に重要なのは、C*はCを共通言語として使用することで、実装と証明コードの開発を統合することです。 私たちはC*のプロトタイプを実装し、小さなCプログラムの代表的なベンチマークと、pKVMのバディアロケータのアタッチ関数という挑戦的な実世界のケーススタディで評価しました。私たちの結果は、C*がCプログラミングのイディオムの広範なサブセットの検証をサポートし、実世界のシナリオにおける複雑な推論タスクを効果的に処理できることを示しています。