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.

翻译：本文介绍了一种用于验证Python程序的工具，该工具通过类型标注与前端处理，能够利用有界模型检验（BMC）流程的功能。它将输入程序转换为抽象语法树，以推断并添加类型信息。随后，将Python表达式与语句翻译为中间表示。最后，将该描述转换为可通过可满足性模理论（SMT）求解器进行求值的公式。所提出的方法通过高效的基于SMT的有界模型检验器（ESBMC）实现，由此产生的工具称为ESBMC-Python，这是首个基于BMC的Python代码验证器。使用为此专门开发的测试套件进行的实验结果表明了其有效性，其中成功与失败的测试均得到了正确评估。此外，该工具在以太坊共识规范中发现了一个实际问题。