SMACK 既是一个模块化软件验证工具链，也是一个独立的软件验证器。它可用于验证输入程序中的断言。在默认模式下，断言会在给定的循环迭代和递归深度边界内进行验证；同时，它也包含对无界验证的实验性支持。SMACK 能处理 C 语言的复杂特性，包括动态内存分配、指针算术和位运算。
在底层，SMACK 是一个将 LLVM 编译器的常用中间表示（IR）转换为 Boogie 中间验证语言（IVL）的翻译器。利用 LLVM IR 可以借助越来越多的编译器前端、优化和分析工具。目前，SMACK 仅通过 Clang 编译器支持 C 语言，但我们正在努力增加对其他语言的支持。以 Boogie 为目标则利用了一个经典平台，简化了验证、模型检查和抽象解释等算法的实现。目前，SMACK 依赖于 Boogie 和 Corral 验证器。
系统要求、安装、使用及其他信息请参见下文。
我们非常重视您使用 SMACK 的感受。如有任何反馈，请随时联系 Zvonimir、Michael 或 Shaobo。
SMACK 项目已获得美国国家科学基金会、VMware、亚马逊和微软研究院的部分资助。我们还依赖犹他大学的 Emulab 基础设施进行广泛的 SMACK 基准测试。
