スマートコントラクトの脆弱性対策に向けた形式検証手法の新たなアプローチ

プログラミング言語に形式仕様の構造を直接組み込むことで、スマートコントラクトの開発に革命をもたらし、その脆弱性を根絶できる可能性がある。

March 12, 2025

Rust における継続渡しスタイル (CPS) の簡略化

本記事では、ローカルメモリポインタと「矢印」ステートメントを活用して抽象的なプログラムを宣言する、先進的な CPS(継続渡しスタイル)の実装例を探ります。

March 25, 2025

コンパイラにおけるアリーナベースの割り当て

アリーナベースの割り当ては、大きなメモリ ブロックを事前割り当てし、そのブロックから多数の小さなオブジェクトをすばやく切り出すメモリ管理戦略です。

February 24, 2025

Cランタイムを理解する

Cランタイム(CRT)は、プログラムが実行されるために必要な初期化ルーチン、ライブラリのサポートコード、システムコールのラッパなどをまとめた仕組みです。本記事では、CRTのスタートアップオブジェクトに含まれる crt0.o、crt1.o、crti.o、crtn.o などのファイルがどのような役割を持ち、なぜ存在するのか、そしてC(およびC++)プログラムがスムーズに動作するためにどのように連携しているのかを解説します。

January 15, 2025

計算機科学における論理入門

このブログでは、「計算機科学における論理」という本で説明されている命題論理の基礎を概説します。

November 9, 2024

TLA+で結婚をコミットする パート2

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

May 1, 2024

TLA+でハードに死なないために パート1

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

April 10, 2024

スモールステップとビッグステップのセマンティクス

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

March 21, 2024

スマートコントラクトのセキュリティにおけるLTLとCTLの応用

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

March 14, 2024

なぜ形式的仕様を使うのか

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

March 4, 2024