はまやんはまやんはまやん

hamayanhamayan's blog

モデル検査とその手法

モデル検査

システムがある性質を満たすかを形式的に検証すること。
システムはプログラムとか仕様でもいい。
ある性質は活性とか、単にこういう値にならないとか。

以下、よく使われる手法。

帰納法

論文
  • 2011年 Software Verification Using k-Induction