OSまたはアプリの実行導出木を有限にする
#GearsOS
#modelchecking
例えば、Queue/BinaryTree/RedBlackTree だけOSを記述する
再帰的なデータ構造は有限な実行導出木に帰着できる(場合がある
するとモデル検査が常に可能になる
プレスバーガーロジック (一次連立不等式)
fairness の問題は file の大きさとかと違って仮定しする必要がある