概要

今日,ネットワークファンクションが仕様に則って安全に動作することを保証するために,そのソフトウェアを検証する手法について研究が行われている.Arseniy ZaostrovnykhらはLazy Proofsを用いてC言語ソフトウェアを検証する手法[1]を提案している.本論文ではF*言語を用いることで彼らとは異なったアプローチでC言語のソフトウェアを検証する手法について提案する.また本手法は複雑な証明の組み合わせなどを用いないため,既存手法よりシンプルに実現できる点が特徴である.

Top