CockroachDB から覗く形式手法の世界

Track E 2020/09/09 18:00-18:40

初級者   Architecture Design   アーカイブ視聴可  

バグのない分散システムの設計は果たして可能でしょうか？
この問いに対する一つの答えとして、CockroachDB では形式手法ツール TLA+ を用いて分散トランザクションの正しさを担保しています。
形式手法はシステムの挙動を数学的に解析する技法で、「ノードが特定のタイミングで故障した場合にのみ発生するバグ」といった再現困難な問題を確実に検出することができます。
本講演では、CockroachDB の事例を通して、形式手法が実世界で活用されている様子をお伝えします。

チェシャ猫
ProofCafe
Software Engineer

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