Towards a Model Checker for Python: pymodcheck

Abstract

Python is a highly popular programming language, used across a broad range of domains from web servers to autonomous robots. Thus, to ensure correctness of these software systems, it is essential to develop good software verification tooling that is useable and well-integrated with Python. To this end we propose a model checker designed specifically for Python that would identify potential errors, and ease the development and testing process. We discuss what would be desirable in such a model checker and present our work in progress, with an approach inspired by Java Pathfinder, along with plans for future development.