SMACK 软件验证工具链

SMACK即是一个模块化的软件验证工具链，又是一个独立的软件验证工具。它可以被用于验证输入程序里的断言。默认模式下SMACK对断言的验证是有对循环/递归的上限。同时，SMACK实现了对无上限的验证的初步支持。SMACK可以处理复杂的C语言特性，如动态内存分配，指针操作，和位运算。

本质上SMACK是一个从LLVM中间语言(IR)到Boogie中间语言的翻译器。使用LLVM IR使得SMACK可以利用大量的支持LLVM IR的编译器，对LLVM IR的优化和分析。目前，SMACK通过Clang编译器实现对C语言的支持。同时，我们也在开发对其他语言的支持。使用Boogie使得SMACK可以利用一个通用的验证平台，该平台简化了对验证方法的实现。目前，SMACK支持Boogie和Corral两个后端验证工具。

SMACK已经用于百度开源项目SGXRay。

对SMACK的安装请参照该文档

对SMACK的使用请参照该文档

对SMACK的使用问题请联系何少博(shaobohe@baidu.com)