Skip to content

benjirewis/vc-generator

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

1 Commit
 
 
 
 
 
 
 
 
 
 

Repository files navigation

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.

About

Verification condition generator built in scala

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages