ESBMC v7.3：使用Clang AST对C++程序进行模型检测
摘要：ESBMC v7.3引入了基于clang的C++前端，作为最新的高效基于SMT的有界语境模型检查器版本。之前的基于CPROVER的前端能够处理C++03程序，但随着C++语言的不断发展，它遇到了许多挑战。随着每个C++版本添加了新的语言和库特性，旧的前端的限制变得明显，导致代码难以维护。因此，现代C++程序的验证变得具有挑战性。为了克服这个障碍，我们重新开发了前端，选择了使用clang的更强大的方法。新的前端使用clang的API高效地遍历内存中的抽象语法树（AST），并将每个AST节点转换为ESBMC的中间表示形式。通过大量的实验，我们的结果表明，带有新前端的ESBMC v7.3显著减少了解析和转换错误，成功验证了各种C++程序，从而优于之前的ESBMC版本。
作者：Kunjian Song, Mikhail R. Gadelha, Franz Brau{ss}e, Rafael S. Menezes, Lucas C. Cordeiro
论文ID：2308.05649
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-08-11