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.10_false-unreach-call_false-termination.cil.c
programSHA 08df5410e85fb22c8b978794a5ef4e5af84949c928d9d8e173b3fb842b1d882d
witnessName results-validated/cpa-seq-validate-violation-witnesses-verifuzz.2018-12-09_1743.logfiles/sv-comp19_prop-reachsafety.token_ring.10_false-unreach-call_false-termination.cil.c.files/witness.graphml
witnessSHA c3c8de64ef8ba8c7d44e4e45f2c40e558a477d54fee7dab853c8c64b5cab14c6

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-09T18:16:00+01:00
inputwitnesshash ad7995a6585e70619c61c7c902b9859e7e82a83abaaa5f01a37ce51f1f02ef63
producer CPAchecker 1.7-svn 29852
program-sha256 08df5410e85fb22c8b978794a5ef4e5af84949c928d9d8e173b3fb842b1d882d
programfile ../../sv-benchmarks/c/systemc/token_ring.10_false-unreach-call_false-termination.cil.c
programhash 08df5410e85fb22c8b978794a5ef4e5af84949c928d9d8e173b3fb842b1d882d
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/c3c8de64ef8ba8c7d44e4e45f2c40e558a477d54fee7dab853c8c64b5cab14c6.graphml
witness-sha256 c3c8de64ef8ba8c7d44e4e45f2c40e558a477d54fee7dab853c8c64b5cab14c6
witness-size 777582
witness-type violation_witness

This witness was created for this program (cf. table above, 08df5410e85fb22c8b978794a5ef4e5af84949c928d9d8e173b3fb842b1d882d).

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

Trying to find witnesses for program (08df5410e85fb22c8b978794a5ef4e5af84949c928d9d8e173b3fb842b1d882d, sv-benchmarks/c/systemc/token_ring.10_false-unreach-call_false-termination.cil.c).

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

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

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

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

Found 8 witnesses for program sv-benchmarks/c/systemc/token_ring.10_false-unreach-call_false-termination.cil.c, 08df5410e85fb22c8b978794a5ef4e5af84949c928d9d8e173b3fb842b1d882d
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/08df5410e85fb22c8b978794a5ef4e5af84949c928d9d8e173b3fb842b1d882d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download af7a91d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 606 2019-12-11T21:41:09+01:00 Download acdf6be
Download edefb5a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 2076 2019-12-11T20:55:18+01:00 Download e23fe60
Download 38497aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 800 2019-12-11T20:44:43+01:00 Download d58afe2
Download 0be5e89 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 606 2019-12-03T08:10:05+01:00 Download f619862
Download f619862 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 622 2019-11-29T18:46:25+01:00
Download acdf6be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 606 2019-12-01T10:36:42+01:00
Download a46298b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 131 2019-12-08T01:51:30+01:00 Download 62bbbef
Download 6d554fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 131 2019-12-05T20:20:35+01:00 Download 7ec048a

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

Trying to find witnesses for program (08df5410e85fb22c8b978794a5ef4e5af84949c928d9d8e173b3fb842b1d882d, sv-benchmarks/c/systemc/token_ring.10_false-unreach-call_false-termination.cil.c).

Found 11 witnesses for program sv-benchmarks/c/systemc/token_ring.10_false-unreach-call_false-termination.cil.c, 08df5410e85fb22c8b978794a5ef4e5af84949c928d9d8e173b3fb842b1d882d
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/08df5410e85fb22c8b978794a5ef4e5af84949c928d9d8e173b3fb842b1d882d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a5fe71f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T20:46 CET (sv-comp)
Download 54c2969 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 75 2018-12-08T09:21:15
Download c3c8de6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 778 2018-12-09T18:16:00+01:00 Download ad7995a
Download c915691 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 607 2018-12-08T23:42:20+01:00 Download a5fe71f
Download ebbbf63 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 606 2018-12-08T22:11:30+01:00 Download 54c2969
Download e26b2ec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 606 2018-12-08T05:02:35+01:00 Download 1c8340c
Download be33170 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 643 2018-12-06T09:18:52+01:00 Download 52486e1
Download 9018fa4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 131 2018-12-10T20:36:27+01:00 Download 303fb59
Download 579a62a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 131 2018-12-06T10:19:20+01:00 Download ba3069d
Download fd8cbc9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 378 2018-12-06T23:27:15+01:00
Download 999cb24 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 378 2018-12-05T18:02:22+01:00

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

Trying to find witnesses for program (08df5410e85fb22c8b978794a5ef4e5af84949c928d9d8e173b3fb842b1d882d, sv-benchmarks/c/systemc/token_ring.10_false-unreach-call_false-termination.cil.c).

Found 9 witnesses for program sv-benchmarks/c/systemc/token_ring.10_false-unreach-call_false-termination.cil.c, 08df5410e85fb22c8b978794a5ef4e5af84949c928d9d8e173b3fb842b1d882d
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/08df5410e85fb22c8b978794a5ef4e5af84949c928d9d8e173b3fb842b1d882d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c35a49c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 304 Sat Dec 2 21:00:24 2017
Download 2d76115 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T16:18 CET (sv-comp)
Download a3ae219 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 51 2017-12-01T15:17:37.058751
Download 2e5dd7c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 23 2017-12-01T10:50:44.555966
Download 592dd6d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 219 2017-12-01T16:38 CET (sv-comp)
Download c10d76d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 219 2017-12-01T01:56 CET (sv-comp)
Download e3a8a58 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 567 2017-11-30T15:30:28+01:00
Download 95c4626 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 299 2017-11-30T23:48 CET (sv-comp)
Download dc0276e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.6.1-svn 26773 376 2017-12-01T17:55:56+01:00

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

Trying to find witnesses for program (08df5410e85fb22c8b978794a5ef4e5af84949c928d9d8e173b3fb842b1d882d, sv-benchmarks/c/systemc/token_ring.10_false-unreach-call_false-termination.cil.c).

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

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