ZetZ、形式的検証機能を備えたCのダイアレクト
原文(投稿日：2020/02/27)へのリンク ZetZ、略してZZは、RustにインスパイアされたCのダイアレクト(diarect, 方言)だ。コンパイル時に仮想マシン内でシンボリック実行することによって、コードの形式的検証を行う。 ZZはハードウェアに近い部分で動作するソフトウェアをターゲットにしているが、クロスプラットフォームなANSI-C準拠のライブラリ構築にも使用することができる。実際には、ZZはCコードのトランスパイラとして、処理結果を任意の標準的Cコンパイラに入力することで動作する。多くの言語が行っている安全性へのアプローチとは対照的に、ZZは、例えば生のポインタアクセスのように"安全でない(unsafe)"と見なした機能の除外や制限は行わない。その代わりに静的単一代入(static single assignment, SSA)を使用して、yices2やz3といったSMTプ
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Z3Py Guide
GitHub - zetzit/zz: 🍺🐙 ZetZ a zymbolic verifier and tranzpiler to bare metal C
