APPLICATION OF Z3 SOLVERS IN THE VERIFICATION SYSTEM FOR PYTHON PROGRAMS
DOI:
https://doi.org/10.32689/maup.it.2023.1.5Keywords:
program verification, correctness condition; symbol execution; counterexample; Z3 solverAbstract
The work describes the latest version of the VerPro program verification system in Python. In order to check the identical truth of the verification conditions, it was supplemented by the solvers of the popular Z3 theorem proving system. The purpose of the article is to describe the new capabilities of the VerPro system, provided by the Z3 solvers. Scientific novelty. The VerPro system is a modern verification system for annotated Python programs that generates correctness conditions by the method of symbolic execution. VerPro provides the user with a modern dialog graphical window interface built using the PyQt5 library. The simplification of these conditions is based on equivalent transformations implemented by the ExprLib library. ExprLib is our own library built in Python without no other dependencies. The library transforms expressions into an internal representation built on the Python language classes. Equivalent transformations implemented in the VerPro system can often establish the identical truth of the verification conditions themselves. If not, then VerPro passes such conditions to the Z3 theorem proving system, which either establishes their identical truth, or builds a counterexample for the hypothesis of the identical truth of such a condition. The presence of a counterexample indicates that the annotation incorrectly describes the functional properties of the program. Analyzing the counterexample found by the system, the user can find the cause of the incorrectness and change the program and/or its annotation. The Z3 system connects to the VerPro via the Z3py software interface. Conclusion. The idea of building counterexamples in program verification systems was implemented for the first time. The Z3 theorem proving system was not previously used in such systems. The VerPro system provides an example of a successful use of a modern theorem proving system not only to establish the correctness of an annotated program, but also to find a solution in case of failed verification. Further development of the system involves the assignment of types for symbolic parameter values and the construction of invariants.
References
Костирко В.С. Система верифікації python–програм. Матеріали ХXV Міжнародної науково-практичній конференції. К.: Європейський університет. 2019. С. 75–78.
Floyd, R. W. Assigning meanings to programs. Proceedings of a Symposium on Applied Mathematics. American Mathematical Society. 19 Mathematical Aspects of Computer Science. 1967. 19–31.
Z3 API in Python. Retrieved from: https://ericpony.github.io/z3py-tutorial/guide-examples.htm.
Костирко, В. С., Плеша, В. І. (2021). Система верифікації програм VerPro. Сучасні напрями розвитку економіки, підприємництва, технологій та їх правового забезпечення: матеріали Міжнародної науково-практичної конференції. Львів: Львівський торговельно-економічний університет. 287–288.
PyQt5 Reference Guide. Retrieved from: https://www.riverbankcomputing.com/ static/Docs/PyQt5/.
Костирко, В.С., Плеша, В. І. Застосування бібліотеки Z3py для перевірки умов коректності та завершимості програм. Матеріали ХXVІ міжнародної науково-практичної інтернет–конференції. К.: Європейський університет. 2020. 80–83.
Wayne, H. Retrieved from: https://github.com/hwayne/lets-prove-leftpad.
Bruni, R., Giacobazzi, R., Gori, R., Ranzato, F. (2023). A Correctness and Incorrectness Program Logic. Journal of the ACM. 70. 1–45. DOI: https://doi.org/10.1145/3582267.
Stump, A. (2016). Verified Functional Programming in Agda. Association for Computing Machinery and Morgan & Claypool. DOI: https://doi.org/10.1145/2841316.
Vardi, M. Y. (2021). Program verification: vision and reality. Communications of the ACM (CACM). 64 (7). 5. DOI: https://doi.org/10.1145/3469113.
