• 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

    http://esbmc.org/

    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

    http://dsverifier.org/

    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

    http://esbmc-gpu.org/

    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