|
|
|
|
|
|
by joshuata
3319 days ago
|
|
|
An interesting solution to this problem is verification witnesses[1]. A witness is a machine readable record of a verification task. Several different programs can read the witness and verify it independently. It is especially useful for counterexamples, where it can be a simple program trace to the error state. Given the input program and witness another can check whether the error state is reached. [1] https://www.sosy-lab.org/~dbeyer/verification-witnesses/ |
|
|