記述集合論に基づく分散システムの階層的特徴付け

Proposal (採択)

上級者   その他    

分散システムの仕様を厳密に記述し自動的に検査する方法論は、古くからの研究テーマである。古典的には時相論理を用いた安全性と活性による定式化が知られていたが、1993 年に Chang らによって提案された Borel 階層による特徴付けは、分散システムの直感的な挙動と数学的な概念との対応をより深く説明している点で興味深い。本講演では、どこかで聞いたような分散システムの解説に飽きてきた中上級者に向け、Chang らの元論文とその関連研究をサーベイする。

Cheshire Cat
ProofCafe
Software Engineer

普段の業務では、Docker や Kubernetes を中心としたコンテナオーケストレーション技術の検証と基盤設計を担当。それと並行してプライベートでは、関数型プログラミングや数理的手法によるソフトウェア検証について研究していたりいなかったりする。トレードマークは猫耳。