-
ESBMC (Efficient SMT-Based Context-Bounded Model Checking)
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
Bernd Fischer 
Denis Nicole 
Felipe Monteiro Hendrio Marques Jeremy Morse 
João Marques 
Lucas Cordeiro Mauro Lopes Mikhail Ramalho Plataformas
Windows e Linux para plataformas de 32 e 64 bits.
-
DSVerifier (Digital Systems Verifier)
DSVerifier é um verificador de modelos para ajudar engenheiros para verificar se há overflow, ciclo limite, erro, o tempo, estabilidade e fase mínima em sistemas digitais, considerando os efeitos de comprimento de palavra finita (FWL - Finite Word Length).
Download
Responsáveis
Eddie Batista 
Hussama Ismail Iury de Bessa 
João Edgar Lucas Cordeiro Mauro Lopes Mikhail Ramalho 
Renato Abreu 
Waldir Sabino -
ESBMC-GPU
O ESBMC-GPU é um verificador de programas baseado nas teorias do módulo da satisfação (Satisfiability Modulo Theories - SMT) para verificar corrida de dados, bloqueio fatal, segurança de ponteiro, violação dos limites de vetores, estouro aritmético, divisão por zero e afirmações especificadas pelo usuário em programas escritos em Compute Unified Device Architecture (CUDA).
Download
Responsáveis
Celso Carvalho Hendrio Marques 
Higo Albuquerque Isabela Silva Lucas Cordeiro Phillipe Pereira Vanessa Santos -
BMCLua
O objetivo do BMCLua é estender as características de ESBMC, que é um verificador de modelos para software embarcado C/C++, para a linguagem de programação Lua. O verificador de modelo ESBMC é baseado em teorias do módulo da satisfação.O BMCLua é executado no sistema operacional Linux, que exige a instalação do software ESBMC e um interpretador Lua. Como o BMCLua é desenvolvido em Java, também é necessário a instalação do JRE para Linux. A versão atual do BMCLua verifica apenas um subconjunto das instruções de linguagem de programação Lua. Uma versão futura, que está sob o desenvolvimento, irá verificar todos os comandos, operadores e estruturas da linguagem de programação Lua.
Responsáveis
Eddie Batista 
Francisco Januário Lucas Cordeiro
- 1