A verification condition generator that takes [IMP language](https://en.wikipedia.org/wiki/IMP_(programming_language) as input. A project for Yale's CPSC 454: Software Analysis and Verification. Built with scala and [sbt](https://www.scala-sbt.org/). Verification conditions can be examined using a local installation of the [Z3](https://github.com/Z3Prover/z3) theorem prover. Use `sbt` to enter the scala build tool, `compile` and `run foo.imp` where `foo.imp` is some syntactically correct IMP program. Verification conditions are shown as standard output and written to `smt_input.txt` in the current directory. Some examples of IMP programs are included in the benchmarks directory.