Z3 Inspector

Z3 inspector is a tool for live preview of progress Z3 is making on a verification attempt. It currently works only from within Boogie.

When you invoke Boogie as:

Boogie myfile.bpl /proverOpt:INSPECTOR=c:/whereever/you/have/Z3Inspector.exe 

it will spawn the Z3Inspector process and forward everything that Z3 sends prefixed with "STATS". The inspector then displays real-time updates of various Z3 runtime statistics (number of conflicts, restarts, quantifier instances and so on) as well as highlights the assertion the prover is currently working on. It should also highlight the path, at least at the BPL level, but I haven't noticed it doing so yet.

The blinking-assertion is implemented as follows: Boogie sends mapping from labels to token information (file name, line number, token value/assertion error message if present). The Inspector then looks for all files mentioned in tokens, and displays the assertions with a few lines of source code context. This way it also works when Boogie is invoked from VCC (i.e. it displays the C file then, not the BPL file), and should also work with Spec#.

Z3 sends the information based on sampling. The Z3 parameter used to control this is:

PROGRESS_SAMPLING_FREQ: unsigned integer, default: 0, frequency for progress output in milliseconds.

By default when INSPECTOR option is specified, Boogie will set it to 100 (i.e. 10 samples/sec).

In particular this means that if some assertion never blinked, it just never got into sampling, and not that the prover didn't prove it. At some point we might make Z3 print the conflict clauses, then we would be sure which assertions are already done. Also it seems that Z3 currently proves the program top-to-bottom (which is what we expect with CASE_SPLIT=3).

The Z3 Inspector is part of the Z3 depot, and thus comes with VCC as a binary.

Future Work

The next step is to have a button in the inspector labeled "show current model". Z3 would then print the current model / labels and Boogie could display it as well. This will allow for inspection of models, while Z3 is running, a feature that has been requested.


Below you can find a screenshot of the tool in action. On the left side, normally the current assertion blinks in red, but the screenshot shows a situation where the tool is done. The black lines are for assertions that took the highest number of samples, clicking either will take you to the source code. Then you have the source view, in green there are assertions and in black the source. Next there are the statistics.


Last edited Aug 13, 2009 at 10:45 AM by MarkHillebrand, version 3


No comments yet.