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/rangesum05_false-unreach-call_true-termination.i
programSHA 925781f4344edc8e64c6e1fefc53ff97309a7c314d387cbd43956ef3a4ebed1e
witnessName results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.rangesum05_false-unreach-call_true-termination.i.files/witness.graphml
witnessSHA 8527e6b6e5e6dc3369d9b848c4e2c27bd63897121bdf5e9720f385b465de3007

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/8527e6b6e5e6dc3369d9b848c4e2c27bd63897121bdf5e9720f385b465de3007.json

Key Value
architecture 32bit
creationtime 2017-11-30T18:01:03+01:00
producer CPAchecker 1.6.1-svn 26725
program-sha256 925781f4344edc8e64c6e1fefc53ff97309a7c314d387cbd43956ef3a4ebed1e
programfile ../../sv-benchmarks/c/reducercommutativity/rangesum05_false-unreach-call_true-termination.i
programhash 1633e43e3f340ce4ae371cafc3d1ea0a9dad5739
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/8527e6b6e5e6dc3369d9b848c4e2c27bd63897121bdf5e9720f385b465de3007.graphml
witness-sha256 8527e6b6e5e6dc3369d9b848c4e2c27bd63897121bdf5e9720f385b465de3007
witness-size 36303
witness-type violation_witness

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

Trying to find witnesses for program (925781f4344edc8e64c6e1fefc53ff97309a7c314d387cbd43956ef3a4ebed1e, sv-benchmarks/c/reducercommutativity/rangesum05_false-unreach-call_true-termination.i).

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

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

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

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

Found 19 witnesses for program sv-benchmarks/c/reducercommutativity/rangesum05_false-unreach-call_true-termination.i, 925781f4344edc8e64c6e1fefc53ff97309a7c314d387cbd43956ef3a4ebed1e
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/925781f4344edc8e64c6e1fefc53ff97309a7c314d387cbd43956ef3a4ebed1e.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 2c9d6e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 2 2019-12-01 02:00:00
Download ac5fade Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 27 2019-12-03T23:27 CET (comp)
Download 2f68b40 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 55 2019-12-11T21:48:33+01:00 Download 276baa3
Download 6521bc9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 55 2019-12-11T21:09:35+01:00 Download 2c9d6e0
Download 34b12ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 55 2019-12-11T20:44:39+01:00 Download 732df2a
Download 6f96c55 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 55 2019-12-08T01:52:07+01:00 Download 54129f1
Download a9813e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 55 2019-12-03T08:57:31+01:00 Download a75719e
Download 0ce24f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 55 2019-12-03T08:09:58+01:00 Download caeabd2
Download caeabd2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 54 2019-11-30T06:16:32+01:00
Download 54129f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 53 2019-12-07T19:39:41+01:00
Download 276baa3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 53 2019-12-01T02:47:55+01:00
Download f7dee9f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 11 2019-12-11T21:30:46+01:00 Download 25b547f
Download 2cdf5af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 11 2019-12-11T20:54:50+01:00 Download b2c56f0
Download 8c343c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 11 2019-12-08T00:26:17+01:00 Download a439a08
Download 491212f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 11 2019-12-07T21:17:44+01:00 Download f93695d
Download 70590fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 11 2019-12-06T02:40:57+01:00 Download 2f8a959
Download 3f71241 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 10 2019-12-05T20:21:53+01:00 Download a0352fe
Download 468adce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 11 2019-12-04T02:58:09+01:00 Download ac5fade
Download 3606347 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T00:20 CET (comp)

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

Trying to find witnesses for program (925781f4344edc8e64c6e1fefc53ff97309a7c314d387cbd43956ef3a4ebed1e, sv-benchmarks/c/reducercommutativity/rangesum05_false-unreach-call_true-termination.i).

Found 22 witnesses for program sv-benchmarks/c/reducercommutativity/rangesum05_false-unreach-call_true-termination.i, 925781f4344edc8e64c6e1fefc53ff97309a7c314d387cbd43956ef3a4ebed1e
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/925781f4344edc8e64c6e1fefc53ff97309a7c314d387cbd43956ef3a4ebed1e.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ae055cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-07T23:37 CET (sv-comp)
Download 037e203 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T05:49:21
Download 63283fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 31 2018-12-07T14:34 CET (sv-comp)
Download 9b7f5f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 48 2018-12-10T17:21:57+01:00
Download 142fe60 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 53 2018-12-07T23:27:08+01:00
Download 7172453 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 54 2018-12-09T20:53:13+01:00 Download 3b866d4
Download a1b7995 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 54 2018-12-09T18:20:00+01:00 Download 491cc46
Download 0b4a2d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 54 2018-12-08T23:43:54+01:00 Download ae055cc
Download ef99541 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 54 2018-12-08T22:09:51+01:00 Download 037e203
Download ec2a983 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 54 2018-12-08T07:51:06+01:00 Download 142fe60
Download 3fbc0f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 54 2018-12-08T03:50:19+01:00 Download e2020e8
Download 2fe75c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 54 2018-12-07T18:47:19+01:00 Download f7f8e2e
Download 1d7a736 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-10T20:37:21+01:00 Download 9b7f5f0
Download ecd6737 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-09T20:36:40+01:00 Download 9bb2ead
Download 89f179a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-09T20:27:18+01:00 Download 6b40b49
Download db34a0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-08T04:54:40+01:00 Download 2ec3468
Download fe3fdcc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-07T17:38:25+01:00 Download 63283fe
Download f48f506 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-06T10:18:57+01:00 Download 4c5304e
Download 6677670 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-06T09:19:55+01:00 Download 8a6917f
Download 923147f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-06T09:18:13+01:00 Download 5b9b5f6
Download d9e55f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T06:01 CET (sv-comp)
Download f8e585b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T09:26 CET (sv-comp)

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

Trying to find witnesses for program (925781f4344edc8e64c6e1fefc53ff97309a7c314d387cbd43956ef3a4ebed1e, sv-benchmarks/c/reducercommutativity/rangesum05_false-unreach-call_true-termination.i).

Found 20 witnesses for program sv-benchmarks/c/reducercommutativity/rangesum05_false-unreach-call_true-termination.i, 925781f4344edc8e64c6e1fefc53ff97309a7c314d387cbd43956ef3a4ebed1e
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/925781f4344edc8e64c6e1fefc53ff97309a7c314d387cbd43956ef3a4ebed1e.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download df7b8bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 3 2017-12-01T22:52 CET (sv-comp)
Download 4f93cc9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VIAP 4 2017-12-03T04:04 CET (sv-comp)
Download db8f117 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 42 2017-12-03T02:39Z
Download 39e1fba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T04:36 CET (sv-comp)
Download 4029e80 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 3 2017-12-01T19:48 CET (sv-comp)
Download 2193e60 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 41 2017-12-02T03:50Z
Download 81234a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 8 2017-12-01T12:53:32.066503
Download 3c4f1b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 8 2017-12-01T08:04:59.618177
Download 580e382 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 15 2017-12-01T20:01 CET (sv-comp)
Download 2be5e6b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 15 2017-11-30T22:47 CET (sv-comp)
Download 0e7347b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 48 2017-12-02T18:37:09+01:00
Download 636fd2d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 50 2017-11-30T18:43:50+01:00
Download 3773b1a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 67 2017-11-30T19:42:16+01:00
Download 8527e6b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 36 2017-11-30T18:01:03+01:00
Download c10ad6e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 29 2017-12-01T21:01:20+01:00
Download 48e2741 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 31 2017-11-30T18:35 CET (sv-comp)
Download 26b531b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 41 2017-12-02T08:30Z
Download 76254cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T02:05:16.025340
Download 5813beb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T14:27:22.293047
Download e70eef2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 31 2017-12-01T16:38 CET (sv-comp)

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

Trying to find witnesses for program (925781f4344edc8e64c6e1fefc53ff97309a7c314d387cbd43956ef3a4ebed1e, sv-benchmarks/c/reducercommutativity/rangesum05_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/reducercommutativity/rangesum05_false-unreach-call_true-termination.i, 925781f4344edc8e64c6e1fefc53ff97309a7c314d387cbd43956ef3a4ebed1e
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/925781f4344edc8e64c6e1fefc53ff97309a7c314d387cbd43956ef3a4ebed1e.json

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