ESBMC v7.3: Model Checking C++ Programs Using Clang AST

  • Kunjian Song University of Manchester
  • Mikhail R. Gadelha Igalia
  • Franz Brauße University of Manchester
  • Rafael S. Menezes University of Manchester
  • Lucas C. Cordeiro University of Manchester

Resumo


This paper introduces ESBMC v7.3, the latest Efficient SMT-Based Context-Bounded Model Checker version, which now incorporates a new Clang-based C++ front-end. While the previous CPROVER-based front-end served well for handling C++03 programs, it encountered challenges keeping up with the evolving C++ language. As new language and library features were added in each C++ version, the limitations of the old front-end became apparent, leading to difficult-to-maintain code. Consequently, modern C++ programs were challenging to verify. To overcome this obstacle, we redeveloped the front-end, opting for a more robust approach using Clang. The new front-end efficiently traverses the Abstract Syntax Tree (AST) in-memory using Clang APIs and transforms each AST node into ESBMC’s Intermediate Representation. Through extensive experimentation, our results demonstrate that ESBMC v7.3 with the new front-end significantly reduces parse and conversion errors, enabling successful verification of a wide range of C++ programs, thereby outperforming previous ESBMC versions.
Palavras-chave: Formal Methods, Model Checking, Software Verification
Publicado
04/12/2023
SONG, Kunjian; GADELHA, Mikhail R.; BRAUSSE, Franz; MENEZES, Rafael S.; CORDEIRO, Lucas C.. ESBMC v7.3: Model Checking C++ Programs Using Clang AST. In: SIMPÓSIO BRASILEIRO DE MÉTODOS FORMAIS (SBMF), 26. , 2023, Manaus/AM. Anais [...]. Porto Alegre: Sociedade Brasileira de Computação, 2023 . p. 141-152.