SMACKは、モジュラーソフトウェア検証ツールチェーン であり、自己完結型ソフトウェア検証器 でもあります。入力プログラム内のアサーションを検証するために使用できます。デフォルトモードでは、アサーションはループ反復と再帰深度に与えられた境界まで検証されます。また、非有界検証のための実験的なサポートも含まれています。SMACKは、動的メモリ割り当て、ポインタ演算、ビット演算など、C言語の複雑な機能を処理します。
内部では、SMACKは LLVM コンパイラの一般的な中間表現（IR）を Boogie 中間検証言語（IVL）に変換するトランスレータです。LLVM IRをソースとすることで、増加するコンパイラフロントエンド、最適化、および解析を活用します。現在、SMACKは Clang コンパイラを介してC言語のみをサポートしていますが、追加の言語のサポートを提供するために取り組んでいます。Boogieをターゲットとすることで、検証、モデル検査、抽象解釈のためのアルゴリズムの実装を簡素化する標準プラットフォームを活用します。現在、SMACKは Boogie および Corral 検証器を利用しています。
システム要件、インストール、使用方法、その他すべてについては以下を参照してください。
SMACKの使用体験をぜひお聞かせください。ご意見・ご感想がありましたら、Zvonimir、Michael、またはShaobo までご連絡ください。
一般的な質問は、最初に FAQ を参照してください。
その他、壊れている場合や不足している場合は、issue を開いてください。
最新情報を入手するには、SMACKのGithubページをウォッチしてください。
SMACKプロジェクトは、米国国立科学財団、VMware、Amazon、Microsoft Researchからの資金提供により部分的に支援されています。また、SMACKの広範なベンチマークのためにユタ大学の Emulab インフラストラクチャも利用しています。
