|
本研究で提案した高レベルプログラムの時相的・関係的検証のためのリファインメント型システム、不動点論理、動的論理といった検証理論・手法は、既存手法が扱えなかった高階関数や代数データ型といった発展的な言語機能を扱うことを可能とした。また、本研究では、提案した検証理論に基づき、高階関数型言語 OCaml のための検証ツール RCaml、不動点論理制約解消ツール MuVal、述語制約解消ツール PCSat の開発も行っており、今後これらのツールを実際のソフトウェア開発現場で実用可能なレベルまで発展させれば、ソフトウェアの信頼性向上に大きく貢献することが期待される。
|
