SMACK既是模块化软件验证工具链,又是独立的软件验证程序。 它可以用来验证其输入程序中的断言。 在默认模式下,对声明进行验证,直到达到循环迭代和递归深度的给定界限为止; 它还包含对无边界验证的实验支持。 SMACK处理C语言的复杂功能,包括动态内存分配,指针算术和按位运算。 在幕后,SMACK是从编译器流行的中间表示(IR)到中间验证语言(IVL)的翻译器。 采购LLVM IR会利用越来越多的编译器前端,优化和分析。 尽管我们正在努力提供对其他语言的支持,但当前SMACK仅通过编译器支持C语言。 Targeting Boogie利用规范平台简化了验证,模型检查和抽象解释算法的实现。 目前,