談話会

アセンブラで書かれたプログラムをモデル検査した事例の報告。モデル化するだけで見つかるエラーは少なくないが、一方で、状態爆発が起こるため実際のモデルを動かすのは大変らしい。