ESBMC-Python: A Bounded Model Checker for Python Programs

本文介绍了一种用于验证Python程序的工具，该工具利用类型注释和前端处理，可以利用有界模型检查（BMC）管道的能力。它将输入程序转换为抽象语法树以推断和添加类型信息。然后，它将Python表达式和语句转换为中间表示。最后，它将此描述转换为使用满足模理论（SMT）求解器评估的公式。所提出的方法是使用高效的基于SMT的有界模型检查器（ESBMC）实现的，从而产生了一个名为ESBMC-Python的工具，这是第一个基于BMC的Python代码验证器。实验结果使用专门为此目的开发的测试套件显示了其有效性，其中成功和失败的测试被正确评估。此外，它在以太坊共识规范中发现了一个真实的问题。

本论文旨在介绍一种验证Python程序的工具，利用类型注释和前端处理，可以利用有界模型检查（BMC）管道的功能。该工具将Python程序转换为抽象语法树以推断和添加类型信息，然后将Python表达式和语句转换为中间表示，最后将此描述转换为使用SMT求解器计算的公式。论文试图解决Python程序验证的问题，并提出了一种新的解决方案。

该工具的关键思路是将Python程序转换为中间表示，然后将其转换为SMT公式进行求解，从而验证其正确性。相比当前的研究状况，该论文的思路具有创新性。

论文使用了一个名为ESBMC-Python的工具来验证Python程序，并提供了一个专门为此目的开发的测试套件。实验结果表明，该工具的有效性得到了验证，并且在以太坊共识规范中发现了一个真正的问题。值得注意的是，该工具还支持类型推理和前置条件的验证。

最近在这个领域中，还有一些相关研究，如：1. “VeriPy: A Tool for Verifying Python Programs”；2. “PyExZ3: Automatic Assertion Generation for Python Programs using Z3 SMT Solver”；3. “Verifying Python Programs with Viper”等。