\chapter{結論}
\label{chapter5}
本稿では、Continuation based C言語による実装と
その実装に対する検証手法を提案した。

第\ref{chapter3}章では、検証の対象として並列プログラムを選択し、
その例題としてDining Philosophers Problemを採用し、実装した。

検証の前準備として、並列プログラムの全状態を網羅的に探索するための
タブロー展開器を実装した。

また、タブロー展開する際に検証用のコードセグメントを組み込むことで
Dining Philosophers Problemのデッドロックを検知できるようにした。

第\ref{chapter4}では、タブロー展開器と
それに検証用コードセグメントを組み込んだ場合のそれぞれの実装において、
プロセス数に対する状態数と検証にかかる時間の評価および考察を行った。

プロセス数が5個の場合の実行時間が0.68秒と高速であり、
実用レベルに達しているといえる。

また、他のモデル検査ツールであるSPINとJava PathFinderとの比較を行い、考察した。
\\

今後の課題として、状態探索にかかる時間を短縮するために
メモリの Binary Tree をバランスさせることと、
状態探索空間を圧縮するために、
LZW法による状態の圧縮の実装をすることがあげられる。