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/bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i
programSHA 6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced
witnessName results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.jain_7_true-unreach-call_true-no-overflow_false-termination.i.files/witness.graphml
witnessSHA fabfa94f4607c00a52c7ba50bc42fbfcfec4000116653e976ba1ff5736fe8137

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-11-30T15:13:55+01:00
producer CPAchecker 1.6.1-svn 26773
program-sha256 6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced
programfile ../../sv-benchmarks/c/bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i
programhash 7d6184439bd2d68a79fcaf77b73b718dbf21eef0
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/fabfa94f4607c00a52c7ba50bc42fbfcfec4000116653e976ba1ff5736fe8137.graphml
witness-sha256 fabfa94f4607c00a52c7ba50bc42fbfcfec4000116653e976ba1ff5736fe8137
witness-size 4225
witness-type correctness_witness

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

Trying to find witnesses for program (6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced, sv-benchmarks/c/bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i, 6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced.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 (6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced, sv-benchmarks/c/bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i, 6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced.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 (6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced, sv-benchmarks/c/bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i, 6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced.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 (6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced, sv-benchmarks/c/bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i, 6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced.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 (6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced, sv-benchmarks/c/bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i, 6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced.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 (6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced, sv-benchmarks/c/bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i).

Found 12 witnesses for program sv-benchmarks/c/bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i, 6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download eb45f44 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 1 2018-12-08T02:52 CET (sv-comp)
Download fefd47c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness SMACK 1.9.3 3 2018-12-08T08:58:53
Download e5e05b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 4 2018-12-08T01:27:43+01:00
Download a4827fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-05T11:22:23+01:00
Download 8ecb51c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T02:23:32
Download 89f2cbc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 4 2018-12-07T01:23:02+01:00
Download ef89523 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:28:51+01:00 Download 569cd22
Download 8e0113b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T20:17:08+01:00 Download f4a613a
Download 199359b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T19:55:46+01:00 Download bb61b09
Download 0a91de5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-05T12:37:10+01:00
Download f8221e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 6 2018-12-06T13:10:55+01:00
Download dd76551 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-05T14:36:57+01:00

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

Trying to find witnesses for program (6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced, sv-benchmarks/c/bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i).

Found 21 witnesses for program sv-benchmarks/c/bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i, 6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 84d368d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Map2Check 3 2017-12-02T00:58 CET (sv-comp)
Download d28f9ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 6 2017-12-03T07:44Z
Download aad4e63 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 1 2017-12-03T04:33 CET (sv-comp)
Download 0bab836 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 6 2017-12-03T10:25Z
Download ba6005f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-02T18:23:50.911976
Download 64af8cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 3.1 6 2017-12-01T13:25 CET (sv-comp)
Download c24cd19 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T11:15:15+01:00
Download 6f289c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 6 2017-12-03T10:24Z
Download ec05237 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 12 2017-12-01T10:28 CET (sv-comp)
Download 023bd82 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T22:43 CET (sv-comp)
Download 5997358 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 6 2017-12-03T05:08Z
Download 6c6d74a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T07:18:01+01:00 3ba4b37
Download 714a5f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T00:29:39+01:00 79f4f26
Download 9c1048d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T00:29:27+01:00 a0f39c3
Download fabfa94 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-11-30T15:13:55+01:00
Download 8cd3dcc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 11 2017-12-01T03:53:44+01:00
Download a990127 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 4 2017-11-30T23:47:00+01:00
Download 044996b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 6 2017-12-02T20:28Z
Download 8ffcc4c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T18:28:52+01:00
Download 520a2cd Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 7 2017-12-03T11:14Z
Download ecf3c43 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 8 2017-12-01T14:36 CET (sv-comp)

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

Trying to find witnesses for program (6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced, sv-benchmarks/c/bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i, 6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/6a8bacdce81a8dd1ae9373269e3e34cade980c80920d4898b38a14df93e5bced.json

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