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).
Key | Value |
programName | sv-benchmarks/c/systemc/token_ring.02_true-unreach-call_false-termination.cil.c |
programSHA | 403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9 |
witnessName | results-verified/cpa-seq.2018-12-05_0546.logfiles/sv-comp19_prop-reachsafety.token_ring.02_true-unreach-call_false-termination.cil.c.files/witness.graphml |
witnessSHA | d9f18efbd9e67241b6bc3829d68c89bbf3d6e013d77ed7c8bccf77781e908d94 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-05T12:46:21+01:00 |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | 403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9 |
programfile | ../../sv-benchmarks/c/systemc/token_ring.02_true-unreach-call_false-termination.cil.c |
programhash | 403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/d9f18efbd9e67241b6bc3829d68c89bbf3d6e013d77ed7c8bccf77781e908d94.graphml |
witness-sha256 | d9f18efbd9e67241b6bc3829d68c89bbf3d6e013d77ed7c8bccf77781e908d94 |
witness-size | 48411 |
witness-type | correctness_witness |
This witness was created for this program (cf. table above, 403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9).
Found 0 witnesses for program sv-benchmarks/c/systemc/token_ring.02_true-unreach-call_false-termination.cil.c, 403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/systemc/token_ring.02_true-unreach-call_false-termination.cil.c, 403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/systemc/token_ring.02_true-unreach-call_false-termination.cil.c, 403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/systemc/token_ring.02_true-unreach-call_false-termination.cil.c, 403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 8 witnesses for program sv-benchmarks/c/systemc/token_ring.02_true-unreach-call_false-termination.cil.c, 403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
91dd8ba | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 48 | 2019-12-11T20:14:36+01:00 | 3ed5f06 | |
205ccbf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 48 | 2019-12-07T23:32:27+01:00 | 462d980 | |
b3271d1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 48 | 2019-12-07T19:44:27+01:00 | 278664a | |
8b32a43 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 48 | 2019-11-30T16:26:40+01:00 | 4107234 | |
4107234 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 48 | 2019-11-30T04:41:29+01:00 | ||
3ed5f06 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 48 | 2019-11-30T20:51:49+01:00 | ||
b7568ad | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.9 | 59 | 2019-11-29T21:28:08+01:00 | ||
6d2ec67 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 59 | 2019-11-30T23:44:35+01:00 |
Found 11 witnesses for program sv-benchmarks/c/systemc/token_ring.02_true-unreach-call_false-termination.cil.c, 403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
782d3fa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T09:34:34 | ||
5b87c0b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 48 | 2018-12-08T02:50:22+01:00 | ||
64a4716 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 49 | 2018-12-09T20:49:10+01:00 | 1007f63 | |
f59c879 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 49 | 2018-12-09T20:17:00+01:00 | ae764ff | |
e06ea83 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 49 | 2018-12-08T21:57:10+01:00 | 782d3fa | |
6c98dda | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 49 | 2018-12-08T07:33:26+01:00 | 5b87c0b | |
dcd43c0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 49 | 2018-12-06T09:42:59+01:00 | a54ae8a | |
acf7095 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 49 | 2018-12-06T09:00:16+01:00 | d9f18ef | |
d9f18ef | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 48 | 2018-12-05T12:46:21+01:00 | ||
d9fb55d | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 59 | 2018-12-08T00:34:01+01:00 | ||
7a3d40f | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 59 | 2018-12-05T19:07:32+01:00 |
Found 10 witnesses for program sv-benchmarks/c/systemc/token_ring.02_true-unreach-call_false-termination.cil.c, 403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
22a4e6f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 48 | 2017-12-03T02:52:55+01:00 | 2a88eca | |
f4a2a6f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 48 | 2017-12-02T14:47:23+01:00 | 28e6bd0 | |
7040929 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 48 | 2017-12-01T07:09:38+01:00 | 6b93477 | |
af40b60 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 48 | 2017-12-01T05:26:39+01:00 | 8b9dfd6 | |
d5d2035 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 48 | 2017-11-30T22:11:55+01:00 | ||
8f5eae5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26725 | 48 | 2017-11-30T18:39:19+01:00 | ||
ea0f4ca | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker (unknown version) | 43 | 2017-12-01T23:32:10+01:00 | ||
9b7f822 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 85 | 2017-12-02T09:17Z | ||
b9d5291 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 59 | 2017-12-01T15:53:21+01:00 | ||
e117692 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Automizer | 43 | 2017-12-03T11:13Z |
Found 0 witnesses for program sv-benchmarks/c/systemc/token_ring.02_true-unreach-call_false-termination.cil.c, 403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/403fe230a852bf1ff90c224c8ad101752c12e041751795435b361434f4f71ae9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |