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_false-unreach-call_false-termination.cil.c |
programSHA | 6c4f5b8391ea3337980198d4bcd1b3615fc8bd481ab77c1328d9280d18cd4655 |
witnessName | results-verified/cbmc.2017-11-30_1120.logfiles/sv-comp18.token_ring.02_false-unreach-call_false-termination.cil.c.files/witness.graphml |
witnessSHA | d566025b5d5777246b4b548b27115186364ea5fe72b3d924c3783d278b8bbbfd |
Key | Value |
architecture | 32bit |
creationtime | 2017-11-30T19:56 CET (sv-comp) |
producer | CBMC |
program-sha256 | 6c4f5b8391ea3337980198d4bcd1b3615fc8bd481ab77c1328d9280d18cd4655 |
programfile | ../../sv-benchmarks/c/systemc/token_ring.02_false-unreach-call_false-termination.cil.c |
programhash | 216b1eba72c80bc0eec8bb9ab0298bf8baf472d8 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/d566025b5d5777246b4b548b27115186364ea5fe72b3d924c3783d278b8bbbfd.graphml |
witness-sha256 | d566025b5d5777246b4b548b27115186364ea5fe72b3d924c3783d278b8bbbfd |
witness-size | 56041 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/systemc/token_ring.02_false-unreach-call_false-termination.cil.c, 6c4f5b8391ea3337980198d4bcd1b3615fc8bd481ab77c1328d9280d18cd4655
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/6c4f5b8391ea3337980198d4bcd1b3615fc8bd481ab77c1328d9280d18cd4655.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_false-unreach-call_false-termination.cil.c, 6c4f5b8391ea3337980198d4bcd1b3615fc8bd481ab77c1328d9280d18cd4655
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/6c4f5b8391ea3337980198d4bcd1b3615fc8bd481ab77c1328d9280d18cd4655.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_false-unreach-call_false-termination.cil.c, 6c4f5b8391ea3337980198d4bcd1b3615fc8bd481ab77c1328d9280d18cd4655
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/6c4f5b8391ea3337980198d4bcd1b3615fc8bd481ab77c1328d9280d18cd4655.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_false-unreach-call_false-termination.cil.c, 6c4f5b8391ea3337980198d4bcd1b3615fc8bd481ab77c1328d9280d18cd4655
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/6c4f5b8391ea3337980198d4bcd1b3615fc8bd481ab77c1328d9280d18cd4655.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 15 witnesses for program sv-benchmarks/c/systemc/token_ring.02_false-unreach-call_false-termination.cil.c, 6c4f5b8391ea3337980198d4bcd1b3615fc8bd481ab77c1328d9280d18cd4655
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/6c4f5b8391ea3337980198d4bcd1b3615fc8bd481ab77c1328d9280d18cd4655.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
d92b118 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 3 | 2019-12-01 06:38:17 | ||
2c411f1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 99 | 2019-12-11T21:45:24+01:00 | dc80ceb | |
4b86489 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 99 | 2019-12-11T21:09:34+01:00 | d92b118 | |
97c4cf7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 269 | 2019-12-11T20:54:53+01:00 | 0a0cb6e | |
a4b6ea4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 105 | 2019-12-11T20:44:37+01:00 | 2b4c003 | |
05ef982 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 99 | 2019-12-08T00:27:11+01:00 | 0ffdac7 | |
40be841 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 99 | 2019-12-07T21:13:44+01:00 | 6cff480 | |
02b3061 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 99 | 2019-12-03T08:57:04+01:00 | a45de0e | |
aa6c6a0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 99 | 2019-12-03T08:08:12+01:00 | 3bd68e9 | |
3bd68e9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 96 | 2019-11-30T14:24:32+01:00 | ||
dc80ceb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 95 | 2019-11-30T20:59:37+01:00 | ||
a0a3234 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 52 | 2019-12-08T01:51:17+01:00 | a67d9ad | |
63d6601 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 51 | 2019-12-05T20:20:48+01:00 | 170d578 | |
8e8975f | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.9 | 62 | 2019-11-29T20:36:11+01:00 | ||
637cb4a | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 62 | 2019-11-30T23:31:47+01:00 |
Found 19 witnesses for program sv-benchmarks/c/systemc/token_ring.02_false-unreach-call_false-termination.cil.c, 6c4f5b8391ea3337980198d4bcd1b3615fc8bd481ab77c1328d9280d18cd4655
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/6c4f5b8391ea3337980198d4bcd1b3615fc8bd481ab77c1328d9280d18cd4655.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e6805fd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T03:05 CET (sv-comp) | ||
8cebe9a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 17 | 2018-12-08T13:49:10 | ||
44b22cf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 99 | 2018-12-07T04:00:39+01:00 | ||
db5af9d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 99 | 2018-12-09T20:53:16+01:00 | 2be10f8 | |
089d9f6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 99 | 2018-12-09T20:38:04+01:00 | aabbd8e | |
e35d8bc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 265 | 2018-12-09T18:20:30+01:00 | 57d25f2 | |
e97a62c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 99 | 2018-12-08T23:44:46+01:00 | e6805fd | |
c735273 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 99 | 2018-12-08T22:11:32+01:00 | 8cebe9a | |
3577cb7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 99 | 2018-12-08T07:52:09+01:00 | 44b22cf | |
5dd77ab | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 99 | 2018-12-08T04:56:50+01:00 | 0b6be31 | |
6543c44 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 99 | 2018-12-08T03:40:36+01:00 | 95beed8 | |
c519232 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 256 | 2018-12-06T10:19:08+01:00 | 7f51696 | |
f4825a4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 99 | 2018-12-06T09:47:56+01:00 | a9d906a | |
882ab50 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 99 | 2018-12-06T09:19:47+01:00 | b99fe09 | |
a9d906a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 96 | 2018-12-05T15:04:14+01:00 | ||
390ad54 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 52 | 2018-12-10T20:37:01+01:00 | bbef48d | |
d9830d8 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 62 | 2018-12-06T13:18:31+01:00 | ||
ba48c93 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 62 | 2018-12-06T10:20:28+01:00 | ||
28e31b2 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 62 | 2018-12-05T13:49:39+01:00 |
Found 14 witnesses for program sv-benchmarks/c/systemc/token_ring.02_false-unreach-call_false-termination.cil.c, 6c4f5b8391ea3337980198d4bcd1b3615fc8bd481ab77c1328d9280d18cd4655
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/6c4f5b8391ea3337980198d4bcd1b3615fc8bd481ab77c1328d9280d18cd4655.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
4513c57 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | VeriAbs 1.3 | 55 | Sat Dec 2 19:16:34 2017 | ||
0fcd8a3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T12:54 CET (sv-comp) | ||
cf6813a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 8 | 2017-12-01T21:51:32.877290 | ||
fa442f9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 7 | 2017-12-01T09:14:15.300610 | ||
0e481af | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 36 | 2017-12-01T16:31 CET (sv-comp) | ||
be76de4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 36 | 2017-12-01T05:01 CET (sv-comp) | ||
eacbf50 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 87 | 2017-12-01T02:03:23+01:00 | ||
809d084 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 110 | 2017-12-01T02:25:54+01:00 | ||
3dfb5fc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 65 | 2017-11-30T16:47:57+01:00 | ||
58f9bf5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 68 | 2017-12-01T23:01:00+01:00 | ||
d566025 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 56 | 2017-11-30T19:56 CET (sv-comp) | ||
be8c8d3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 117 | 2017-12-02T02:22Z | ||
97f2cb7 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 61 | 2017-12-01T18:12:08+01:00 | ||
c99ffe6 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Automizer | 43 | 2017-12-03T11:12Z |
Found 0 witnesses for program sv-benchmarks/c/systemc/token_ring.02_false-unreach-call_false-termination.cil.c, 6c4f5b8391ea3337980198d4bcd1b3615fc8bd481ab77c1328d9280d18cd4655
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/6c4f5b8391ea3337980198d4bcd1b3615fc8bd481ab77c1328d9280d18cd4655.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |