What is it about?

ESBMC-Python is a model checking tool that verifies Python programs using Bounded Model Checking (BMC). It translates Python code into an Intermediate Representation (IR), and uses SMT solvers to verify safety properties like the absence of runtime errors (e.g., buffer overflows, division by zero) and the correctness of assertions.

Featured Image

Read the Original

This page is a summary of: ESBMC-Python: A Bounded Model Checker for Python Programs, September 2024, ACM (Association for Computing Machinery),
DOI: 10.1145/3650212.3685304.
You can read the full text:

Read

Contributors

The following have contributed to this page