smackers/smackChaîne d'outils modulaire de vérification logicielle qui traduit le LLVM IR en langage de vérification intermédiaire Boogie pour la vérification d'assertions bornée et expérimentale non bornée dans des programmes C.
SMACK est à la fois une chaîne d'outils modulaire de vérification logicielle et un vérificateur logiciel autonome. Il peut être utilisé pour vérifier les assertions dans ses programmes d'entrée. Dans son mode par défaut, les assertions sont vérifiées jusqu'à une limite donnée sur le nombre d'itérations de boucles et la profondeur de récursion ; il contient également un support expérimental pour la vérification non bornée. SMACK gère les fonctionnalités complexes du langage C, notamment l'allocation dynamique de mémoire, l'arithmétique des pointeurs et les opérations bit à bit.
Sous le capot, SMACK est un traducteur de la LLVM représentation intermédiaire (IR) populaire du compilateur vers le Boogie langage de vérification intermédiaire (IVL). Le fait de se baser sur LLVM IR exploite un nombre croissant de fronts de compilation, d'optimisations et d'analyses. Actuellement, SMACK ne supporte que le langage C via le compilateur Clang, bien que nous travaillions à fournir un support pour d'autres langages. Cibler Boogie exploite une plateforme canonique qui simplifie l'implémentation d'algorithmes de vérification, de model checking et d'interprétation abstraite. Actuellement, SMACK utilise les vérificateurs Boogie et Corral.
Voir ci-dessous pour les prérequis système, l'installation, l'utilisation et tout le reste.
Nous sommes très intéressés par votre expérience avec SMACK. N'hésitez pas à contacter Zvonimir, Michael ou Shaobo pour tout retour possible.
Pour des questions générales, consultez d'abord la FAQ.
Si quelque chose est cassé ou manquant, ouvrez un issue.
En dernier recours, envoyez un courriel à Michael, Zvonimir, et Shaobo.
Pour rester informé des mises à jour, vous pouvez surveiller la page Github de SMACK.
Le projet SMACK a été partiellement soutenu par des financements de la National Science Foundation, VMware, Amazon et Microsoft Research. Nous nous appuyons également sur l'infrastructure Emulab de l'Université de l'Utah pour des tests de performance approfondis de SMACK.
