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.05_false-unreach-call_false-termination.cil.c
programSHA 67f17d241855a9901f114dd291327bddc683c73c94ceeb6b2deca9c270796981
witnessName results-verified/esbmc-kind.2018-12-06_1103.logfiles/sv-comp19_prop-reachsafety.token_ring.05_false-unreach-call_false-termination.cil.c.files/witness.graphml
witnessSHA 05268f365f81c2097d51377a3434aecebe0c2fdcda1028870b1702d4e88e2a83

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/05268f365f81c2097d51377a3434aecebe0c2fdcda1028870b1702d4e88e2a83.json

Key Value
architecture 32bit
creationtime 2018-12-06T11:30:46.160406
producer ESBMC 6.0.0 kind
programfile ../../sv-benchmarks/c/systemc/token_ring.05_false-unreach-call_false-termination.cil.c
programhash 27d160802d278384ef6d8db395ef2d19702d5645
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/05268f365f81c2097d51377a3434aecebe0c2fdcda1028870b1702d4e88e2a83.graphml
witness-sha256 05268f365f81c2097d51377a3434aecebe0c2fdcda1028870b1702d4e88e2a83
witness-size 10837
witness-type violation_witness

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

Trying to find witnesses for program (67f17d241855a9901f114dd291327bddc683c73c94ceeb6b2deca9c270796981, sv-benchmarks/c/systemc/token_ring.05_false-unreach-call_false-termination.cil.c).

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

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

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

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

Found 14 witnesses for program sv-benchmarks/c/systemc/token_ring.05_false-unreach-call_false-termination.cil.c, 67f17d241855a9901f114dd291327bddc683c73c94ceeb6b2deca9c270796981
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/67f17d241855a9901f114dd291327bddc683c73c94ceeb6b2deca9c270796981.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 48fb107 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 4 2019-12-01 18:56:07
Download 0a6b86e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 237 2019-12-11T21:40:43+01:00 Download 8bfe98b
Download 21aa9ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 237 2019-12-11T21:09:41+01:00 Download 48fb107
Download 5f96dca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 742 2019-12-11T20:54:30+01:00 Download 3a39667
Download 6193265 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 237 2019-12-11T20:44:36+01:00 Download a5d1507
Download e77ecc0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 237 2019-12-08T00:26:08+01:00 Download ee2e93f
Download de4e5a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 237 2019-12-07T21:18:11+01:00 Download 7816749
Download 46c38ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 237 2019-12-03T08:10:35+01:00 Download a37472c
Download a37472c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 230 2019-11-30T00:18:41+01:00
Download 8bfe98b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 237 2019-12-01T01:37:14+01:00
Download c8cb8f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 81 2019-12-08T01:51:19+01:00 Download 36c7fd4
Download 8e742a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 81 2019-12-05T20:21:42+01:00 Download 752a159
Download 05e9556 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.9 147 2019-11-30T12:12:49+01:00
Download 3c3d6c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 147 2019-12-01T02:51:45+01:00

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

Trying to find witnesses for program (67f17d241855a9901f114dd291327bddc683c73c94ceeb6b2deca9c270796981, sv-benchmarks/c/systemc/token_ring.05_false-unreach-call_false-termination.cil.c).

Found 16 witnesses for program sv-benchmarks/c/systemc/token_ring.05_false-unreach-call_false-termination.cil.c, 67f17d241855a9901f114dd291327bddc683c73c94ceeb6b2deca9c270796981
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/67f17d241855a9901f114dd291327bddc683c73c94ceeb6b2deca9c270796981.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 02ab35d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T13:03 CET (sv-comp)
Download b8cd13d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 35 2018-12-08T06:31:58
Download 2f8f7b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 239 2018-12-07T17:59:38+01:00
Download 0fca05e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 273 2018-12-09T18:21:11+01:00 Download 96d259a
Download 415e08f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 238 2018-12-08T23:44:34+01:00 Download 02ab35d
Download 91ae580 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 237 2018-12-08T22:09:00+01:00 Download b8cd13d
Download ee2d7a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 237 2018-12-08T08:45:47+01:00 Download 2f8f7b1
Download 08f61b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 237 2018-12-08T05:02:17+01:00 Download 05268f3
Download 79f1b27 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 541 2018-12-06T10:17:50+01:00 Download e369aae
Download 81344b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 237 2018-12-06T09:48:03+01:00 Download 4b2e090
Download 57431d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 265 2018-12-06T09:18:09+01:00 Download d96d216
Download 4b2e090 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 230 2018-12-05T05:55:18+01:00
Download e1fefb3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 82 2018-12-10T20:35:08+01:00 Download 08c70ab
Download 747bae1 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 147 2018-12-07T08:04:21+01:00
Download 9f1ff1e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 150 2018-12-06T10:14:29+01:00
Download 2ef99ff Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 147 2018-12-06T06:51:01+01:00

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

Trying to find witnesses for program (67f17d241855a9901f114dd291327bddc683c73c94ceeb6b2deca9c270796981, sv-benchmarks/c/systemc/token_ring.05_false-unreach-call_false-termination.cil.c).

Found 12 witnesses for program sv-benchmarks/c/systemc/token_ring.05_false-unreach-call_false-termination.cil.c, 67f17d241855a9901f114dd291327bddc683c73c94ceeb6b2deca9c270796981
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/67f17d241855a9901f114dd291327bddc683c73c94ceeb6b2deca9c270796981.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b8085cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 230 Sun Dec 3 00:41:16 2017
Download 18560bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T00:05 CET (sv-comp)
Download 7f0d34a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 14 2017-12-01T14:31:59.867429
Download 8f86a37 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 12 2017-12-01T13:55:39.319322
Download da7ad42 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 66 2017-12-01T19:52 CET (sv-comp)
Download fc80efe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 66 2017-12-01T01:46 CET (sv-comp)
Download 5a1fa95 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 208 2017-11-30T20:42:16+01:00
Download b51beb0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 260 2017-12-01T02:35:31+01:00
Download 615a600 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 153 2017-11-30T13:50:50+01:00
Download 0ad8c56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 127 2017-11-30T19:17 CET (sv-comp)
Download f97ec2e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.6.1-svn 26773 146 2017-12-01T15:22:39+01:00
Download 147b4b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 71 2017-12-03T11:13Z

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

Trying to find witnesses for program (67f17d241855a9901f114dd291327bddc683c73c94ceeb6b2deca9c270796981, sv-benchmarks/c/systemc/token_ring.05_false-unreach-call_false-termination.cil.c).

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

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