Blogs

レスリー・ランポートによる「TLA+入門」コースのコンスペクトの第1部。

このブログでは、スモールステップとビッグステップのセマンティクス、その違い、コンピュータプログラムの分析への応用について概説します。

このブログでは、線形時相論理および計算木論理を探求し、それらをどのようにスマートコントラクトの検証に使用できるかを説明します。

このブログでは、プログラム検証の文脈で形式的仕様の利点を探ります。