This project is read-only.
The Boogie Verification Debugger (BVD) is a tool with an interface akin to that of dynamic debuggers. It lets users learn more about failed verifications by inspecting the values of variables in the counterexample provided by the theorem prover. BVD currently has plug-ins for VCC and for Dafny, and it works with Z3 as the theorem prover.

Using BVD with VCC

You need to use VCC3, i.e., the new VCC memory model. Run VCC as follows:

  vcc -3 -cev:foo.model foo.c


This will create file "foo.model", then run:

  bvd foo.model

Using BVD with Dafny

Run:

  dafny -mv:foo.model foo.dfy


This will create file "foo.model", then run:

  bvd foo.model

Using BVD with Boogie

Run:

  boogie -mv:foo.model foo.bpl


This will create file "foo.model", then run:

  bvd foo.model


Note that the model is displayed with no interpretation, and thus might be huge and confusing.

Last edited Mar 10, 2011 at 1:39 AM by rustanleino, version 1

Comments

No comments yet.