from 形式手法

モデル検査と形式仕様記述の事例が載ってる

Compilerの仕様の検証

入力言語と、出力言語の各意味を数式で表現することで、

任意の入力に対して、出力が同じものを表すことを示すことができる

OS

独自にKMLという形式仕様記述言語を作ってCOROの検証をしたらしい

分散システムの検証

自動テストの代わりに形式手法を使う

AWSで使われている