This project is read-only.

Generate counter-example

Nov 13, 2009 at 2:37 PM

When VCC proves that C program fails, Model Viewer can show counter-example. Did you use model cheking to find counter-example?

I'm interested in generating counter-example. Can you tell me more detail about it?

Thank alot

Nov 13, 2009 at 3:30 PM
Edited Nov 13, 2009 at 4:33 PM

Model checking has nothing to do with this.

VCC uses Boogie to generate verification conditions, which are then passed to the SMT solver Z3 to be proven or refuted. For a very approachable introduction to this process, for example check Michal's PhD thesis at http://research.microsoft.com/en-us/um/people/moskal/pdf/phd.pdf .

The resulting logic formula is built such that it is unsatisfiable if and only if the program has the desired properties. On the other hand, if the program fails verification, this means that the formula is satisfiable. For a satisfiable formula, Z3 can be instructed to construct a model, which satisfies the formula and thus is a counter example for the verification condition.

The model viewer attempts to translate such a model back into a more human-readable form.

Mar 21, 2010 at 4:15 PM
Edited Mar 21, 2010 at 4:15 PM

Could you explain to me what is Z3 model (counter example)? Please give me some examples too! Thank you very much

Mar 24, 2010 at 2:10 PM

The purpose of the Z3 model is described in the thesis cited above. To view the counter example for a failed verification, run vcc with the /m switch. This will produce a .vccmodel file that contains the Z3 counter example. You can inspect this file using the Z3 Axiom Profiler, which is installed with the VCC tools.