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).

View and Validate the Witness

Input Given to this Service about the Witness (URL Query)

Key Value
programName sv-benchmarks/c/reducercommutativity/avg20_true-unreach-call.i
programSHA de7a81d8613067d5938c80af80a28eca3ca61edd7ce7ae85a7ffa5dc3a8ba6dc
witnessName results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.avg20_true-unreach-call.i.files/witness.graphml
witnessSHA 65fb3b81c07c3df52db04e65b0c7d079216cf81977625c2b46e11611599bc847

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/65fb3b81c07c3df52db04e65b0c7d079216cf81977625c2b46e11611599bc847.json

Key Value
architecture 32bit
creationtime 2017-11-30T22:02 CET (sv-comp)
memoryModel precise
producer ESBMC 3.1
program-sha256 de7a81d8613067d5938c80af80a28eca3ca61edd7ce7ae85a7ffa5dc3a8ba6dc
programfile /tmp/vcloud-vcloud-master/worker/working_dir_3977917d-7425-40ce-8b7f-263b9bd9e0e8/sv-benchmarks/c/reducercommutativity/avg20_true-unreach-call.i
programhash f5e81652b9257047806afb0da3b85390243a03ff
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/65fb3b81c07c3df52db04e65b0c7d079216cf81977625c2b46e11611599bc847.graphml
witness-sha256 65fb3b81c07c3df52db04e65b0c7d079216cf81977625c2b46e11611599bc847
witness-size 27794
witness-type correctness_witness

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

Trying to find witnesses for program (de7a81d8613067d5938c80af80a28eca3ca61edd7ce7ae85a7ffa5dc3a8ba6dc, sv-benchmarks/c/reducercommutativity/avg20_true-unreach-call.i).

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 80df78c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-04T01:21 CET (comp)
Download 77ce4a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 8 2019-12-11T20:25:42+01:00 Download ba58856
Download b7a4dd5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 8 2019-12-08T00:36:18+01:00 Download 36d131d
Download a44fb07 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 8 2019-12-06T01:43:07+01:00 Download 1239f52
Download ac6bfbc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 8 2019-12-04T02:08:00+01:00 Download 80df78c
Download b75dd7f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 8 2019-11-30T19:01:01+01:00 Download bc588ac
Download e7d0649 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 8 2019-11-30T16:11:37+01:00 Download c897203
Download c897203 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 16 2019-11-30T07:21:30+01:00

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

Trying to find witnesses for program (de7a81d8613067d5938c80af80a28eca3ca61edd7ce7ae85a7ffa5dc3a8ba6dc, sv-benchmarks/c/reducercommutativity/avg20_true-unreach-call.i).

Found 15 witnesses for program sv-benchmarks/c/reducercommutativity/avg20_true-unreach-call.i, de7a81d8613067d5938c80af80a28eca3ca61edd7ce7ae85a7ffa5dc3a8ba6dc
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/de7a81d8613067d5938c80af80a28eca3ca61edd7ce7ae85a7ffa5dc3a8ba6dc.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 2d6bec6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T09:39 CET (sv-comp)
Download 8f09830 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T06:25:12
Download 77c2b1b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T00:34 CET (sv-comp)
Download 18dfcb5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 16 2018-12-08T02:05:47+01:00
Download ba9209c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-10T20:18:50+01:00 Download d643c38
Download 40794c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-09T21:21:34+01:00 Download 1cb17b1
Download d56fc84 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-08T23:37:11+01:00 Download 2d6bec6
Download 375a515 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-08T21:53:31+01:00 Download 8f09830
Download 38b13f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T07:34:37+01:00 Download 18dfcb5
Download 66083db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-08T02:03:47+01:00 Download ff82957
Download 1267f1c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-07T18:00:49+01:00 Download 00c56cb
Download 20f9d74 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-07T16:53:21+01:00 Download 77c2b1b
Download 5695124 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:43:07+01:00 Download 4ea6e1c
Download eed4f98 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-06T09:00:19+01:00 Download 74701fe
Download 74701fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-05T21:58:42+01:00

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

Trying to find witnesses for program (de7a81d8613067d5938c80af80a28eca3ca61edd7ce7ae85a7ffa5dc3a8ba6dc, sv-benchmarks/c/reducercommutativity/avg20_true-unreach-call.i).

Found 12 witnesses for program sv-benchmarks/c/reducercommutativity/avg20_true-unreach-call.i, de7a81d8613067d5938c80af80a28eca3ca61edd7ce7ae85a7ffa5dc3a8ba6dc
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/de7a81d8613067d5938c80af80a28eca3ca61edd7ce7ae85a7ffa5dc3a8ba6dc.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 63fa9b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 163 2017-11-30T14:09:32+01:00
Download cf1182f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 83 2017-11-30T21:53:44+01:00
Download 00c56cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T23:37 CET (sv-comp)
Download 0e9eb8b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T19:19 CET (sv-comp)
Download 7fb2908 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 5 2017-12-01T21:01 CET (sv-comp)
Download 65fb3b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 28 2017-11-30T22:02 CET (sv-comp)
Download a5810c0 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 1be5044 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-03T04:34:24+01:00 2b09a39
Download d10ef7c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-02T20:36:16+01:00 83fdd96
Download 40617de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-02T00:26:06+01:00 10f9556
Download df429fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-01T22:25:16+01:00 ad439af
Download 4cfc805 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-01T08:28:43+01:00 d1ffb9d

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

Trying to find witnesses for program (de7a81d8613067d5938c80af80a28eca3ca61edd7ce7ae85a7ffa5dc3a8ba6dc, sv-benchmarks/c/reducercommutativity/avg20_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/reducercommutativity/avg20_true-unreach-call.i, de7a81d8613067d5938c80af80a28eca3ca61edd7ce7ae85a7ffa5dc3a8ba6dc
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/de7a81d8613067d5938c80af80a28eca3ca61edd7ce7ae85a7ffa5dc3a8ba6dc.json

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