|
ソフトウェアに対して信頼性の高い保証を与える技術として、形式検証が注目されている。しかし、ソフトウェアはＣやアセンブリなどの低レベル言語で書かれると、技術的な詳細が多くなるため、現状では形式検証による安全性の完全な保証はまだ困難である。本研究では組込み応用向けのプログラムの検証のため、プラットフォームによって異なる意味論を表現し、C言語のモデルとその論理を形式化した。具体的には、共通の形式定理のライブラリに基づき、アセンブリ言語とC言語、それぞれの形式検証基盤を構築し、現実的なケーススタディーを用いてその有効性を確かめ、以上の検証実験を公開した。
|
