Trabalho em anais de evento
SMT-Based Bounded Model Checking of C++ Programs
RAMALHO, MIKHAIL; FREITAS, MAURO; SOUSA, FELIPE; MARQUES, HENDRIO; Cordeiro, Lucas; FISCHER, BERND
Resumo
Resumo
Bounded model checking of C++ programs presents greater challenges than that of C programs due to the more complex features that the language offers, such as templates, containers, and exception handling. We present ESBMC++, a bounded model checker for C++ programs. It is based on an operational model, an abstract representation of the standard C++ libraries that conservatively approximates their semantics. ESBMC++ uses this to encode the verification conditions using different background theories supported by an SMT solver. Our experimental results show that our approach can handle a wider range of the C++ constructs than existing approaches and substantially reduces the verification time.
Autoria
Autores do grupo (1)
A lista completa de autores está no topo da página. Abaixo, apenas os pesquisadores do e-Controls vinculados a esta publicação.
palavras-chave
Palavras-chave
bounded model checkingC programsESBMCSMT solversC++ standard libraryoperational semanticstemplatescontainersexception handlingverification conditionsbackground theory
Status
Published
links
Links e arquivos
Trabalho em anais de evento