ESBMC-Python: A Bounded Model Checker for Python Programs

TL;DR

ESBMC-Python is the first bounded model checker designed for verifying Python programs, leveraging type annotations and SMT solvers to detect errors and verify correctness effectively.

Contribution

This paper presents ESBMC-Python, a novel bounded model checking tool specifically for Python, integrating type inference, translation to SMT, and verification capabilities.

Findings

Successfully verified Python programs using ESBMC-Python.

Detected a real bug in the Ethereum Consensus Specification.

Achieved correct evaluation of both passing and failing tests.

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.