VCC3

VCC3 uses a new, more high-level memory model. It has also redesigned background axiomatization. As a consequence it tends to be about an order of magnitude faster than VCC2, at least on recursive data-structure benchmarks.

Additionally, VCC3 is supported by the new Boogie Verification Debugger (available in Boogie source and binary distributions). The BVD improves over current VCC Model Viewer by displaying more of the ghost state, providing search facilities and so on.

Status

VCC3 passes about 70% of the VCC2 testsuite.

Features unsupported at the moment

  • memory reinterpretation
  • unions
  • as_array as fields of structs
  • skinny expose
  • support for various array predicates is patchy

Neither one of these is a theoretical problem, so if there is strong demand, they can be implemented.

Usage

Invoke VCC with "-3" flag to enable VCC3. It implies "-it" (trigger inference) and "-z:CASE_SPLIT=5" (custom Z3 case-split strategy that makes it go faster; its effects with VCC2 are mixed).

To use the BVD, supply the "-cev:filename.model" switch. In case of verification errors it will produce a file named "filename.model", which you need to pass as a command line argument to BVD.

Last edited Dec 17, 2010 at 11:39 PM by MichalMoskal, version 2

Comments

No comments yet.