Model Checking Python Programs with MSVL

To verify the correctness of Python programs, a novel approach for model checking Python programs with MSVL (Modeling, Simulation and Verification Language) is advocated. To this end, the rules for decoding the object-oriented semantics of Python with the process-oriented semantics of MSVL are defined, and the technique for automatically rewriting a Python program into its equivalent MSVL program is formalized, which in turn can be verified with the model checking tool MSV. In addition, an example is given to illustrate how the approach works. The approach fully utilizes the powerful expressiveness of MSVL to verify Python programs in a direct way, and helps to improve the quality of the software system.