smackers/smackCadena de herramientas modular de verificación de software que traduce LLVM IR al lenguaje de verificación intermedio Boogie para la verificación de aserciones acotada y experimentalmente no acotada en programas C.
SMACK es tanto una herramienta modular de verificación de software como un verificador de software autocontenido. Se puede utilizar para verificar las aserciones en sus programas de entrada. En su modo predeterminado, las aserciones se verifican hasta un límite dado en iteraciones de bucles y profundidad de recursión; también cuenta con soporte experimental para verificación sin límite. SMACK maneja características complejas del lenguaje C, incluyendo asignación dinámica de memoria, aritmética de punteros y operaciones a nivel de bits.
Internamente, SMACK es un traductor desde la representación intermedia (IR) popular del compilador LLVM al lenguaje de verificación intermedio (IVL) Boogie. Al utilizar la IR de LLVM, se aprovecha un número creciente de frontends de compiladores, optimizaciones y análisis. Actualmente, SMACK solo admite el lenguaje C a través del compilador Clang, aunque estamos trabajando para brindar soporte para lenguajes adicionales. Al apuntar a Boogie, se explota una plataforma canónica que simplifica la implementación de algoritmos para verificación, model checking e interpretación abstracta. Actualmente, SMACK aprovecha los verificadores Boogie y Corral.
A continuación, se presentan los requisitos del sistema, la instalación, el uso y todo lo demás.
Estamos muy interesados en conocer su experiencia usando SMACK. Por favor, no dude en contactar a Zvonimir, Michael o Shaobo con cualquier comentario.
El proyecto SMACK ha sido parcialmente financiado por la National Science Foundation, VMware, Amazon y Microsoft Research. También contamos con la infraestructura Emulab de la Universidad de Utah para realizar pruebas exhaustivas de SMACK.
