ESBMC-Python: A Bounded Model Checker for Python Programs

Bruno Farias; Rafael Menezes; Eddie B. de Lima Filho; Youcheng Sun; Lucas Cordeiro

ESBMC-Python: A Bounded Model Checker for Python Programs

Bruno Farias, Rafael Menezes, Eddie B. de Lima Filho, Youcheng Sun, Lucas Cordeiro

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

10 Downloads (Pure)

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.

Original language	English
Title of host publication	The ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA)
Publication status	Accepted/In press - 26 Jul 2024

Keywords

Formal Verification
Bounded Model Checking
Python

Access to Document

2407.03472v1Submitted manuscript, 319 KB

Embargoed Document

issta2024_1
Accepted author manuscript, 571 KB
Licence: CC BY
Embargo ends: 29/07/25

Cite this

@inproceedings{08f799739b614fd68590b42095741f43,

title = "ESBMC-Python: A Bounded Model Checker for Python Programs",

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. ",

keywords = "Formal Verification, Bounded Model Checking, Python",

author = "Bruno Farias and Rafael Menezes and Filho, {Eddie B. de Lima} and Youcheng Sun and Lucas Cordeiro",

year = "2024",

month = jul,

day = "26",

language = "English",

booktitle = "The ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA)",

}

TY - GEN

T1 - ESBMC-Python

T2 - A Bounded Model Checker for Python Programs

AU - Farias, Bruno

AU - Menezes, Rafael

AU - Filho, Eddie B. de Lima

AU - Sun, Youcheng

AU - Cordeiro, Lucas

PY - 2024/7/26

Y1 - 2024/7/26

N2 - 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.

AB - 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.

KW - Formal Verification

KW - Bounded Model Checking

KW - Python

M3 - Conference contribution

BT - The ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA)

ER -

ESBMC-Python: A Bounded Model Checker for Python Programs

Abstract

Keywords

Access to Document

Embargoed Document

Fingerprint

Cite this