smackers/smackToolchain modular de verificação de software que traduz LLVM IR para a linguagem de verificação intermediária Boogie para verificação de asserções limitadas e experimentalmente ilimitadas em programas C.
SMACK é tanto uma cadeia de ferramentas modular de verificação de software quanto um verificador de software autocontido. Pode ser usado para verificar as asserções nos programas de entrada. No seu modo padrão, as asserções são verificadas até um determinado limite de iterações de laço e profundidade de recursão; também contém suporte experimental para verificação ilimitada. SMACK lida com recursos complexos da linguagem C, incluindo alocação dinâmica de memória, aritmética de ponteiros e operações bit a bit.
Por baixo dos panos, SMACK é um tradutor da LLVM representação intermediária (IR) popular do compilador para a linguagem de verificação intermediária (IVL) do Boogie. A utilização da IR da LLVM explora um número crescente de front-ends, otimizações e análises de compiladores. Atualmente, SMACK só suporta a linguagem C através do compilador Clang, embora estejamos a trabalhar para fornecer suporte a outras linguagens. A segmentação do Boogie explora uma plataforma canónica que simplifica a implementação de algoritmos para verificação, model checking e interpretação abstrata. Atualmente, SMACK aproveita os verificadores Boogie e Corral.
Veja abaixo os requisitos do sistema, instalação, uso e tudo mais.
Estamos muito interessados na sua experiência com SMACK. Por favor, contacte Zvonimir, Michael ou Shaobo com qualquer feedback possível.
Para perguntas gerais, consulte primeiro o FAQ.
Se algo estiver avariado ou em falta, abra um issue.
Como último recurso, envie um email para Michael, Zvonimir e Shaobo.
Para se manter informado sobre atualizações, pode seguir a página do SMACK no Github.
O projeto SMACK foi parcialmente apoiado por financiamento da National Science Foundation, VMware, Amazon e Microsoft Research. Também contamos com a infraestrutura Emulab da Universidade de Utah para testes extensivos do SMACK.
