SMT_VST : COS 597B: Project
We want to instrument VST with the interface to use CVC4. This includes the ability to translate VST assertions to and from smt-lib 2.0. It will also require the adaptation of CVC4 to deal with the kind of queries specifically generated by VST.