smackers/smackМодульный инструментарий верификации ПО, который транслирует LLVM IR в промежуточный верификационный язык Boogie для ограниченной и экспериментальной неограниченной проверки утверждений в C-программах.
SMACK — это одновременно модульный набор инструментов для верификации программного обеспечения и самодостаточный верификатор программ. Он может использоваться для проверки утверждений во входных программах. В стандартном режиме утверждения проверяются до заданного предела количества итераций циклов и глубины рекурсии; также имеется экспериментальная поддержка безграничной верификации. SMACK обрабатывает сложные возможности языка C, включая динамическое выделение памяти, арифметику указателей и побитовые операции.
Под капотом SMACK является транслятором из популярного промежуточного представления (IR) компилятора LLVM в промежуточный язык верификации (IVL) Boogie. Использование LLVM IR открывает доступ к растущему числу фронтендов компиляторов, оптимизаций и анализов. В настоящее время SMACK поддерживает только язык C через компилятор Clang, хотя мы работаем над поддержкой других языков. Нацеливание на Boogie использует каноническую платформу, которая упрощает реализацию алгоритмов верификации, проверки моделей и абстрактной интерпретации. В настоящее время SMACK использует верификаторы Boogie и Corral.
Ниже приведены системные требования, установка, использование и всё остальное.
Нам очень интересен ваш опыт использования SMACK. Пожалуйста, свяжитесь с , или с любыми возможными отзывами.
Проект SMACK частично финансировался Национальным научным фондом, VMware, Amazon и Microsoft Research. Мы также используем инфраструктуру Emulab Университета Юты для обширного тестирования производительности SMACK.
