Visualize correctness witnesses

mutilin / klever

Klever Git repository read-only mirror

https://forge.ispras.ru/projects/klever

Apache License 2.0

0 stars 1 forks source link

Visualize correctness witnesses #52

Closed vmordan closed 5 years ago

vmordan commented 5 years ago

They can be used as a correctness proof, which currently is missing. Similarly to the error traces, they can be processed into internal format, visualized, compared, marked, edited.

PavelAndrianov commented 5 years ago

The main question is how they will be processed. It's not obvious, because just show graph edges, like in error trace, will confuse a user.

vmordan commented 5 years ago

Currently they have plain structure (no call stack) and mostly show conditions. Therefore, the internal format may include such conditions, which can be compared, marked, etc. Visualization may contain source files with highlighted conditions (and, maybe, some other elements, which present in the witness) or just a list of such conditions.

I think, that only experienced users will ever look at them.

PavelAndrianov commented 5 years ago

It would be much better to have more clear representation, which would be used by other users, like sv-comp participants. Anyway, we may start from a such draft and improve it step by step.

vmordan commented 5 years ago

Commit 15ea2dbd adds first version of correctness witnesses visualization.

Currently there are some limitations:

only one correctness witness is supported per verification task;
correctness witnesses are not supported for Unknown or Unsafe verdicts;
correctness witnesses cannot be edited;
correctness witnesses cannot be compared (as well as error traces).