ESBMC-Python：一个面向 Python 程序的有界模型检查器
ESBMC-Python: A Bounded Model Checker for Python Programs
AI总结：
本文提出 ESBMC-Python，首个基于有界模型检查的 Python 代码验证器，通过类型注解、中间表示转换和 SMT 求解实现程序验证，并在以太坊共识规范中发现真实问题。
摘要：
本文介绍了一种用于验证 Python 程序的工具，该工具利用类型注解和前端处理，能够发挥有界模型检查（BMC）流水线的能力。它将输入程序转换为抽象语法树，以推断并添加类型信息。然后，它将 Python 表达式和语句翻译为一种中间表示。最后，它将该描述转换为用可满足性模理论（SMT）求解器求值的公式。所提出的方法通过高效的基于 SMT 的有界模型检查器（ESBMC）实现，从而产生了一个名为 ESBMC-Python 的工具，这是第一个基于 BMC 的 Python 代码验证器。使用专门为此目的开发的测试套件进行的实验结果表明了其有效性，其中成功和失败的测试均被正确评估。此外，它还在以太坊共识规范中发现了一个真实问题。
英文摘要：
This paper introduces a tool for verifying Python programs, which, using type annotation and front-end processing, can harness the capabilities of a bounded model-checking (BMC) pipeline. It transforms an input program into an abstract syntax tree to infer and add type information. Then, it translates Python expressions and statements into an intermediate representation. Finally, it converts this description into formulae evaluated with satisfiability modulo theories (SMT) solvers. The proposed approach was realized with the efficient SMT-based bounded model checker (ESBMC), which resulted in a tool called ESBMC-Python, the first BMC-based Python-code verifier. Experimental results, with a test suite specifically developed for this purpose, showed its effectiveness, where successful and failed tests were correctly evaluated. Moreover, it found a real problem in the Ethereum Consensus Specification.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
