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/systemc/token_ring.04_false-unreach-call_false-termination.cil.c
programSHA 00c4513318e86646da07f829242d967bc000b2a88688483fce1e8035456130a1
witnessName results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.token_ring.04_false-unreach-call_false-termination.cil.c.files/witness.graphml
witnessSHA 287e768a7a5061ec18aa49e5829eeb4acdb55c2e53e2992319559b97ddda2c6c

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-11-30T16:06:44+01:00
producer CPAchecker 1.6.1-svn 26773
program-sha256 00c4513318e86646da07f829242d967bc000b2a88688483fce1e8035456130a1
programfile ../../sv-benchmarks/c/systemc/token_ring.04_false-unreach-call_false-termination.cil.c
programhash 5e27a879cb97b2b6600a7b4379c4e090f4fa709a
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/287e768a7a5061ec18aa49e5829eeb4acdb55c2e53e2992319559b97ddda2c6c.graphml
witness-sha256 287e768a7a5061ec18aa49e5829eeb4acdb55c2e53e2992319559b97ddda2c6c
witness-size 162178
witness-type violation_witness

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

Trying to find witnesses for program (00c4513318e86646da07f829242d967bc000b2a88688483fce1e8035456130a1, sv-benchmarks/c/systemc/token_ring.04_false-unreach-call_false-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/systemc/token_ring.04_false-unreach-call_false-termination.cil.c, 00c4513318e86646da07f829242d967bc000b2a88688483fce1e8035456130a1
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/00c4513318e86646da07f829242d967bc000b2a88688483fce1e8035456130a1.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 (00c4513318e86646da07f829242d967bc000b2a88688483fce1e8035456130a1, sv-benchmarks/c/systemc/token_ring.04_false-unreach-call_false-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/systemc/token_ring.04_false-unreach-call_false-termination.cil.c, 00c4513318e86646da07f829242d967bc000b2a88688483fce1e8035456130a1
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/00c4513318e86646da07f829242d967bc000b2a88688483fce1e8035456130a1.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 (00c4513318e86646da07f829242d967bc000b2a88688483fce1e8035456130a1, sv-benchmarks/c/systemc/token_ring.04_false-unreach-call_false-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/systemc/token_ring.04_false-unreach-call_false-termination.cil.c, 00c4513318e86646da07f829242d967bc000b2a88688483fce1e8035456130a1
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/00c4513318e86646da07f829242d967bc000b2a88688483fce1e8035456130a1.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 (00c4513318e86646da07f829242d967bc000b2a88688483fce1e8035456130a1, sv-benchmarks/c/systemc/token_ring.04_false-unreach-call_false-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/systemc/token_ring.04_false-unreach-call_false-termination.cil.c, 00c4513318e86646da07f829242d967bc000b2a88688483fce1e8035456130a1
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/00c4513318e86646da07f829242d967bc000b2a88688483fce1e8035456130a1.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 (00c4513318e86646da07f829242d967bc000b2a88688483fce1e8035456130a1, sv-benchmarks/c/systemc/token_ring.04_false-unreach-call_false-termination.cil.c).

Found 15 witnesses for program sv-benchmarks/c/systemc/token_ring.04_false-unreach-call_false-termination.cil.c, 00c4513318e86646da07f829242d967bc000b2a88688483fce1e8035456130a1
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/00c4513318e86646da07f829242d967bc000b2a88688483fce1e8035456130a1.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c491f59 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 4 2019-12-01 07:37:15
Download 4180661 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 184 2019-12-11T21:56:42+01:00 Download 933ad94
Download 40cb163 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 184 2019-12-11T21:09:28+01:00 Download c491f59
Download 0d2ba55 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 557 2019-12-11T20:54:32+01:00 Download 2616322
Download 2eb34ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 324 2019-12-11T20:44:56+01:00 Download 83180e0
Download 77d3310 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 184 2019-12-08T00:26:41+01:00 Download eea4129
Download 70138f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 184 2019-12-07T21:18:13+01:00 Download 5775f02
Download d57041c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 185 2019-12-03T08:57:28+01:00 Download eb1d5d4
Download 5f4358d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 184 2019-12-03T08:12:35+01:00 Download f5ff076
Download f5ff076 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 178 2019-11-30T13:28:28+01:00
Download 933ad94 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 175 2019-11-30T23:11:50+01:00
Download b8660fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 72 2019-12-08T01:51:45+01:00 Download e53919d
Download 31256c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 71 2019-12-05T20:20:26+01:00 Download 5be8e14
Download 51994d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.9 114 2019-11-30T03:12:52+01:00
Download 0b4d5d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 114 2019-12-01T00:25:49+01:00

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

Trying to find witnesses for program (00c4513318e86646da07f829242d967bc000b2a88688483fce1e8035456130a1, sv-benchmarks/c/systemc/token_ring.04_false-unreach-call_false-termination.cil.c).

Found 18 witnesses for program sv-benchmarks/c/systemc/token_ring.04_false-unreach-call_false-termination.cil.c, 00c4513318e86646da07f829242d967bc000b2a88688483fce1e8035456130a1
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/00c4513318e86646da07f829242d967bc000b2a88688483fce1e8035456130a1.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5a847b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T08:22 CET (sv-comp)
Download 73f3f01 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 29 2018-12-08T13:02:11
Download a559705 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 186 2018-12-07T22:00:31+01:00
Download 2e2fab6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 184 2018-12-09T20:39:44+01:00 Download 3e6e7f0
Download 46b86d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 184 2018-12-09T18:20:58+01:00 Download 4aea7af
Download 71c3853 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 185 2018-12-08T23:43:20+01:00 Download 5a847b6
Download c3d13cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 184 2018-12-08T22:09:41+01:00 Download 73f3f01
Download c07dd08 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 184 2018-12-08T08:26:22+01:00 Download a559705
Download da6d6a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 184 2018-12-08T05:06:04+01:00 Download 225d21f
Download b46592c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 185 2018-12-08T04:15:49+01:00 Download 05fba55
Download 748d4f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 409 2018-12-06T10:19:51+01:00 Download d7ce98f
Download 46d6dcb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 184 2018-12-06T09:47:57+01:00 Download a483e12
Download fc0dd5c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 184 2018-12-06T09:17:44+01:00 Download a418af6
Download a483e12 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 178 2018-12-06T06:00:56+01:00
Download 29f6114 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 72 2018-12-10T20:36:14+01:00 Download cc98078
Download 121d01c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 114 2018-12-07T05:20:13+01:00
Download 5ddba95 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 117 2018-12-06T10:20:33+01:00
Download 4df232c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 114 2018-12-06T05:49:49+01:00

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

Trying to find witnesses for program (00c4513318e86646da07f829242d967bc000b2a88688483fce1e8035456130a1, sv-benchmarks/c/systemc/token_ring.04_false-unreach-call_false-termination.cil.c).

Found 13 witnesses for program sv-benchmarks/c/systemc/token_ring.04_false-unreach-call_false-termination.cil.c, 00c4513318e86646da07f829242d967bc000b2a88688483fce1e8035456130a1
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/00c4513318e86646da07f829242d967bc000b2a88688483fce1e8035456130a1.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8668264 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 121 Sun Dec 3 00:21:04 2017
Download 9730e18 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T11:16 CET (sv-comp)
Download 1b36f2d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 11 2017-12-02T02:31:13.918930
Download 10af30f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 10 2017-12-01T11:40:57.164469
Download 0b7f51a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 49 2017-12-01T19:31 CET (sv-comp)
Download 5719c58 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 49 2017-11-30T23:18 CET (sv-comp)
Download 287e768 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 162 2017-11-30T16:06:44+01:00
Download cd93c9c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 202 2017-11-30T16:02:28+01:00
Download 73bda7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 120 2017-11-30T12:02:16+01:00
Download 6c8a748 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 103 2017-12-01T03:47 CET (sv-comp)
Download 75b4a0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 214 2017-12-02T21:05Z
Download b6b1977 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.6.1-svn 26773 114 2017-12-01T13:16:27+01:00
Download e3ce230 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 61 2017-12-03T11:16Z

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

Trying to find witnesses for program (00c4513318e86646da07f829242d967bc000b2a88688483fce1e8035456130a1, sv-benchmarks/c/systemc/token_ring.04_false-unreach-call_false-termination.cil.c).

Found 0 witnesses for program sv-benchmarks/c/systemc/token_ring.04_false-unreach-call_false-termination.cil.c, 00c4513318e86646da07f829242d967bc000b2a88688483fce1e8035456130a1
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/00c4513318e86646da07f829242d967bc000b2a88688483fce1e8035456130a1.json

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