一句话：提出首个基于有界模型检测的 Python 程序验证工具，借助类型标注与 SMT 求解器实现自动化验证。
本文提出 ESBMC-Python，一个用于验证 Python 程序的工具。它利用类型标注和前端处理，将输入程序转换为抽象语法树，并据此推断和补充类型信息；随后把 Python 表达式与语句翻译为中间表示，最终编码为可由 SMT 求解器判定的公式，从而接入高效的有界模型检测（BMC）流水线。该方法在 ESBMC 基础上实现，作者称其为首个基于 BMC 的 Python 代码验证器。实验使用专门开发的测试套件进行评估，结果表明工具能够正确判定成功与失败的测试用例。此外，ESBMC-Python 还在 Ethereum 共识规范中发现了一个真实问题，验证了其在实际代码中的缺陷发现能力。
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.
@inproceedings{paperbot8491,
title = {ESBMC-Python: A Bounded Model Checker for Python Programs},
author = {Bruno Farias and Rafael Menezes and Eddie B. de Lima Filho and Youcheng Sun and Lucas C. Cordeiro},
booktitle = {ISSTA},
year = {2024},
doi = {10.1145/3650212.3685304}
}