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 (5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142, ../../../comp/sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i).

Found 0 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i, 5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142.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 (5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142, ../../../comp/sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i).

Found 0 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i, 5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142.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 (5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142, ../../../comp/sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i).

Found 0 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i, 5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142.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 (5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142, ../../../comp/sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i).

Found 0 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i, 5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142.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 (5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142, ../../../comp/sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i).

Found 8 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i, 5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e5f7ced Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-04T00:43 CET (comp)
Download 21358de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 8 2019-12-11T20:17:15+01:00 Download 22b3897
Download 056e1e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 8 2019-12-08T00:52:38+01:00 Download 4a67e22
Download 82cb0e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 8 2019-12-06T01:44:03+01:00 Download 7fc6752
Download c766465 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 8 2019-12-04T02:07:57+01:00 Download e5f7ced
Download f09cec6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 8 2019-11-30T19:29:59+01:00 Download 6145904
Download 955cd3d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 8 2019-11-30T16:28:10+01:00 Download 7d2e8b2
Download 7d2e8b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 22 2019-11-30T04:47:42+01:00

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

Trying to find witnesses for program (5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142, ../../../comp/sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i).

Found 14 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i, 5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download acb5e8b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T19:02 CET (sv-comp)
Download 037f4b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T07:35:55
Download 727be27 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T11:09 CET (sv-comp)
Download bb35636 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 22 2018-12-07T21:53:03+01:00
Download f7498b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-10T19:50:57+01:00 Download 9e0b780
Download 94c41c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-09T21:21:15+01:00 Download d88cd27
Download cd45ea3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-08T23:24:50+01:00 Download acb5e8b
Download ee530c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-08T21:49:39+01:00 Download 037f4b1
Download e4b5f16 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-08T05:44:22+01:00 Download bb35636
Download b33061b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-08T02:36:06+01:00 Download 73bf8f2
Download 693f2e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-07T16:53:47+01:00 Download 727be27
Download e731d7e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:43:30+01:00 Download 0a2956f
Download f1d1d53 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-06T09:27:50+01:00 Download d3cc162
Download d3cc162 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 22 2018-12-05T14:19:45+01:00

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

Trying to find witnesses for program (5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142, ../../../comp/sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i).

Found 9 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i, 5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e8a99a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 311 2017-11-30T15:25:24+01:00
Download 03ad2b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 158 2017-11-30T12:38:26+01:00
Download 6195c08 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 118 2017-12-01T22:40:36+01:00
Download adb29e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T23:26 CET (sv-comp)
Download bb3f8bb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-01T23:03 CET (sv-comp)
Download 7d5393d 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 22fb72f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-03T04:13:50+01:00 59399a3
Download b5eaee3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773