Formal verification to ensuring the memory safety of C++ Programs

Abstract

Este trabalho descreve e avalia o Efficient SMT-Based Context-Bounded Model Checker (ESBMC) para verificar formalmente programas C++. O ESBMC implementa a técnica de verificação de modelos limitados (do inglês, bounded model checking -- BMC) com base em teorias do módulo da satisfabilidade (do inglês, satisfiability modulo theories -- SMT) para lidar com recursos complexos que a linguagem de programação C++ oferece, tais como templates, contêineres sequenciais e associativos, herança, polimorfismo e manipulação de exceções. ESBMC é comparado as ferramentas LLBMC e DIVINE, as quais verificam os programas C++ diretamente a nível de bitcode do LLVM. Resultados experimentais mostram que o ESBMC pode lidar com uma ampla gama de estruturas do C++, apresentando uma taxa de aproximadamente 85% de verificações corretas e, ao mesmo tempo, reduzindo o tempo de verificação se comparado as ferramentas LLBMC e DIVINE.