本セッションでは、分散システムのような複雑な仕様や動作を持つプログラムに対して、様相論理を用いてその仕様を記述し検査する技術について解説します。 我々はシステムの仕様を保証する際、テスト設計や自動化ツールのような、仕様を「テストする」ための方法論を考えがちです。しかし、その前に仕様が「記述できる…