Python

ESBMC-Python is a frontend for ESBMC that enables formal verification of Python programs. It converts Python source code into ESBMC’s internal representation, allowing the engine to apply bounded model checking and SMT-based reasoning to detect bugs, assertion violations, and undefined behavior.

In This Section

• Overview — Architecture, pipeline stages, and how the frontend works
• Usage — How to install prerequisites, invoke ESBMC on Python files, and interpret results
• Supported Features — Full reference of supported language constructs, data structures, and standard library modules
• Limitations — Known restrictions in the current version
• Pytest Test Generation — Automatic generation of pytest test cases from counterexamples
• Random Operational Model — Details on the random module stub