Profile

Masanori Ogino 𓀁

181351 posts 1993 follows 1215 followers

Please pay attention to random failures.

https://mstdn.maud.io/@omasanori

Masanori Ogino 𓀁 omasanori@mstdn.maud.io

AWSにおける形式手法 - masateruk’s blog masateruk.hatenablog.com/entry

「AWSにおける形式手法の記事( lamport.azurewebsites.net/tla/ )を読んだ。特に重要だと思われる示唆を3つあげると以下の通り。

・産業界では長年形式手法は多大な工数をかけて比較的容易なコードの断片を検証するというイメージがあったが、これはまったくの誤り。現実の問題に適用可能である
・アマゾンでは10の現実のシステムに適用して、すべてで効果が得られた。難解なバグの発見したり、正当性を犠牲にすることなく確信を持って最適化を施せた
・7つのチームでTLA+を使用。エンジニアは2−3週間で学習することができる」