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