PyVerify

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

Dependencies

To run, install lark-parser from

$ pip install lark-parser

and Z3 from

https://github.com/Z3Prover/z3

License

PyVerify uses the MIT license.