O ESBMC é um verificador de programas baseado nas teorias do módulo da satisfação que permite a verificação de programas sequências e multitarefa criados em C/C++ e que compartilham uma mesma região de memória. A ferramenta suporta o padrão ANSI-C e C++ e desta forma consegue verificar programas que fazem uso de vetores, ponteiros, estruturas, uniões, alocação dinâmica de memória e aritmética de ponto fixo. O ESBMC consegue verificar propriedades relacionadas a underflow e overflow aritméticos, segurança de ponteiros, vazamento de memória, violação dos limites de vetores, violações de atomicidade, bloqueio fatal, corrida de dados, e assertivas definidas pelo usuário.
Download
Responsáveis
|
|
|
|
|
|
|
|
|
Plataformas
Windows e Linux para plataformas de 32 e 64 bits.
Redes Sociais