English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

This paper introduces ESBMC v7.3, the latest Efficient SMT-BasedContext-Bounded Model Checker version, which now incorporates a new clang-basedC++ front-end. While the previous CPROVER-based front-end served well forhandling C++03 programs, it encountered challenges keeping up with the evolvingC++ language. As new language and library features were added in each C++version, the limitations of the old front-end became apparent, leading todifficult-to-maintain code. Consequently, modern C++ programs were challengingto verify. To overcome this obstacle, we redeveloped the front-end, opting fora more robust approach using clang. The new front-end efficiently traverses theAbstract Syntax Tree (AST) in-memory using clang APIs and transforms each ASTnode into ESBMC's Intermediate Representation. Through extensiveexperimentation, our results demonstrate that ESBMC v7.3 with the new front-endsignificantly reduces parse and conversion errors, enabling successfulverification of a wide range of C++ programs, thereby outperforming previousESBMC versions.

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