A simple Hoare triple verification condition generator. Analyzes .imp files. IMP structure is given by imp.lark. To run, type
$ python imp_parser.py mult.imp
To run, install lark-parser from
$ pip install lark-parser
and Z3 from
https://github.com/Z3Prover/z3
PyVerify uses the MIT license.