CertAlloc – TLA+ と CBMC により形式的検証された O(1) メモリアロケータ
CertAlloc は、TLA+ と CBMC を用いて形式的検証が行われた O(1) メモリアロケータです。従来のメモリ割り当て手法と比較して、定数時間での動作を保証しながら、メモリ安全性を数学的に証明している点が特徴です。このプロジェクトは GitHub 上で公開されており、信頼性の高いメモリ管理を必要とするシステムへの応用が期待されます。
背景メモ
CertAllocは、TLA+（仕様記述言語）とCBMC（C言語の有界モデル検査器）を用いて形式的検証（フォーマル・ベリフィケーション）が行われたO(1)メモリアロケータ。通常のmalloc/freeは最悪ケースの実行時間が予測困難だが、CertAllocは割り当て・解放を常に一定時間（O(1)）で行うことを保証する。