Witness Inspection

A description of this web service can be found in the CAV paper "Verification-Aided Debugging: An Interactive Web-Service for Exploring Error Witnesses" (more material).

This link does not point to a witness, but below is a list of witnesses for the same program.

Available Results for the Program from Witness Store SV-COMP '24

Trying to find witnesses for program (30ec58ae95cc8577989e64bf4ba2db9e0a8dd29b72d75944713a8f49e3b91364, sv-benchmarks/c/array-examples/standard_running_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/array-examples/standard_running_true-unreach-call.i, 30ec58ae95cc8577989e64bf4ba2db9e0a8dd29b72d75944713a8f49e3b91364
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/30ec58ae95cc8577989e64bf4ba2db9e0a8dd29b72d75944713a8f49e3b91364.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness

Available Results for the Program from Witness Store SV-COMP '23

Trying to find witnesses for program (30ec58ae95cc8577989e64bf4ba2db9e0a8dd29b72d75944713a8f49e3b91364, sv-benchmarks/c/array-examples/standard_running_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/array-examples/standard_running_true-unreach-call.i, 30ec58ae95cc8577989e64bf4ba2db9e0a8dd29b72d75944713a8f49e3b91364
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/30ec58ae95cc8577989e64bf4ba2db9e0a8dd29b72d75944713a8f49e3b91364.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness

Available Results for the Program from Witness Store SV-COMP '22

Trying to find witnesses for program (30ec58ae95cc8577989e64bf4ba2db9e0a8dd29b72d75944713a8f49e3b91364, sv-benchmarks/c/array-examples/standard_running_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/array-examples/standard_running_true-unreach-call.i, 30ec58ae95cc8577989e64bf4ba2db9e0a8dd29b72d75944713a8f49e3b91364
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/30ec58ae95cc8577989e64bf4ba2db9e0a8dd29b72d75944713a8f49e3b91364.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness

Available Results for the Program from Witness Store SV-COMP '21

Trying to find witnesses for program (30ec58ae95cc8577989e64bf4ba2db9e0a8dd29b72d75944713a8f49e3b91364, sv-benchmarks/c/array-examples/standard_running_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/array-examples/standard_running_true-unreach-call.i, 30ec58ae95cc8577989e64bf4ba2db9e0a8dd29b72d75944713a8f49e3b91364
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/30ec58ae95cc8577989e64bf4ba2db9e0a8dd29b72d75944713a8f49e3b91364.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness

Available Results for the Program from Witness Store SV-COMP '20

Trying to find witnesses for program (30ec58ae95cc8577989e64bf4ba2db9e0a8dd29b72d75944713a8f49e3b91364, sv-benchmarks/c/array-examples/standard_running_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/array-examples/standard_running_true-unreach-call.i, 30ec58ae95cc8577989e64bf4ba2db9e0a8dd29b72d75944713a8f49e3b91364
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/30ec58ae95cc8577989e64bf4ba2db9e0a8dd29b72d75944713a8f49e3b91364.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness

Available Results for the Program from Witness Store SV-COMP '19

Trying to find witnesses for program (30ec58ae95cc8577989e64bf4ba2db9e0a8dd29b72d75944713a8f49e3b91364, sv-benchmarks/c/array-examples/standard_running_true-unreach-call.i).

Found 6 witnesses for program sv-benchmarks/c/array-examples/standard_running_true-unreach-call.i, 30ec58ae95cc8577989e64bf4ba2db9e0a8dd29b72d75944713a8f49e3b91364
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/30ec58ae95cc8577989e64bf4ba2db9e0a8dd29b72d75944713a8f49e3b91364.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 664375b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T08:17 CET (sv-comp)
Download 8dfc695 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T02:02:52
Download 20c3c0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-10T20:32:09+01:00 Download 0e062ea
Download b78e4b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-09T21:21:11+01:00 Download 78b82fd
Download ffa4372 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-08T23:21:33+01:00 Download 664375b
Download 0b7f3b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-08T21:52:08+01:00 Download 8dfc695

Available Results for the Program from Witness Store SV-COMP '18

Trying to find witnesses for program (30ec58ae95cc8577989e64bf4ba2db9e0a8dd29b72d75944713a8f49e3b91364, sv-benchmarks/c/array-examples/standard_running_true-unreach-call.i).

Found 4 witnesses for program sv-benchmarks/c/array-examples/standard_running_true-unreach-call.i, 30ec58ae95cc8577989e64bf4ba2db9e0a8dd29b72d75944713a8f49e3b91364
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/30ec58ae95cc8577989e64bf4ba2db9e0a8dd29b72d75944713a8f49e3b91364.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 4b78d55 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 5 2017-12-01T21:48 CET (sv-comp)
Download dd6b057 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.12-svcomp17 4 2017-11-02T13:16:17+05:30
Download cb69e05 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-03T04:36:26+01:00 d0b95ba
Download 018da4f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-01T22:34:19+01:00 9412e4e

Available Results for the Program from Witness Store SV-COMP '17

Trying to find witnesses for program (30ec58ae95cc8577989e64bf4ba2db9e0a8dd29b72d75944713a8f49e3b91364, sv-benchmarks/c/array-examples/standard_running_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/array-examples/standard_running_true-unreach-call.i, 30ec58ae95cc8577989e64bf4ba2db9e0a8dd29b72d75944713a8f49e3b91364
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/30ec58ae95cc8577989e64bf4ba2db9e0a8dd29b72d75944713a8f49e3b91364.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness