ESBMC-Python: A Bounded Model Checker for Python Programs

TL;DR

This paper addresses the challenge of statically verifying Python programs with bounded model checking by introducing ESBMC-Python, a front-end that converts Python code into an AST, enriches it with type information, and feeds it into ESBMC’s SMT-based verification pipeline. The approach reuses ESBMC’s GOTO/SSA-based backend to generate verification conditions of the form $VC = C \land \neg P$ and solve them with SMT solvers. Empirical evaluation on a benchmark of 85 programs across 15 categories shows mean verification times around $31.56$ ms and memory under $30$ MB, while correctly identifying violations and, notably, discovering a real division-by-zero bug in the Ethereum consensus specification. The work demonstrates the practicality and impact of applying BMC to Python, offering a reproducible baseline for Python verification in software security and blockchain domains.

Abstract

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.

Figures (2)

• Figure 1: ESBMC-Python architecture.
• Figure 2: ESBMC-Python output.