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/ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i |
programSHA | 581839242835660c7049651d3b011957f2644fd34c14926011425d9d7608c10b |
witnessName | results-verified/skink.2018-12-07_1200.logfiles/sv-comp19_prop-reachsafety.mutex_lock_int_true-termination.c_false-unreach-call.i.files/witness.graphml |
witnessSHA | cb3bab808ae0eb0f93cd39bb4138f7ebec3417e92cfc6ebe840c280dae455edf |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-07T16:01 CET (sv-comp) |
memorymodel | simple |
producer | skink |
programfile | ../../sv-benchmarks/c/ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i |
programhash | c976dd79cabe443ac09b5b35c5674998e922b27b |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/cb3bab808ae0eb0f93cd39bb4138f7ebec3417e92cfc6ebe840c280dae455edf.graphml |
witness-sha256 | cb3bab808ae0eb0f93cd39bb4138f7ebec3417e92cfc6ebe840c280dae455edf |
witness-size | 2502 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i, 581839242835660c7049651d3b011957f2644fd34c14926011425d9d7608c10b
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/581839242835660c7049651d3b011957f2644fd34c14926011425d9d7608c10b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i, 581839242835660c7049651d3b011957f2644fd34c14926011425d9d7608c10b
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/581839242835660c7049651d3b011957f2644fd34c14926011425d9d7608c10b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i, 581839242835660c7049651d3b011957f2644fd34c14926011425d9d7608c10b
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/581839242835660c7049651d3b011957f2644fd34c14926011425d9d7608c10b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i, 581839242835660c7049651d3b011957f2644fd34c14926011425d9d7608c10b
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/581839242835660c7049651d3b011957f2644fd34c14926011425d9d7608c10b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 21 witnesses for program sv-benchmarks/c/ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i, 581839242835660c7049651d3b011957f2644fd34c14926011425d9d7608c10b
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/581839242835660c7049651d3b011957f2644fd34c14926011425d9d7608c10b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ef90a9f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2019-12-02 02:36:27 | ||
fed4596 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 5 | 2019-12-03T22:38 CET (comp) | ||
4150167 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-11T21:59:14+01:00 | 7832e15 | |
10c7dc9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-11T21:41:11+01:00 | 4dc2b90 | |
81ec3c6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-11T21:09:14+01:00 | ef90a9f | |
f425a43 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-11T20:54:30+01:00 | 4b36f24 | |
1587e2c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-11T20:44:53+01:00 | f099031 | |
e7b7b34 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-08T01:51:15+01:00 | a680930 | |
bb9b2c7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-08T00:26:37+01:00 | 57a3eb7 | |
a942a93 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-08T00:06:01+01:00 | ecd8106 | |
e19ef45 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-07T21:18:21+01:00 | b95ad2d | |
179b5af | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-06T02:38:34+01:00 | 168ce45 | |
a9bc283 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-05T20:21:47+01:00 | 55895a1 | |
cd87caf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-05T19:34:23+01:00 | 52eb134 | |
a9ac686 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-04T02:58:03+01:00 | fed4596 | |
b2ec4ff | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-03T08:56:49+01:00 | c3ea960 | |
f2590fc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-03T08:00:53+01:00 | f804166 | |
f804166 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 6 | 2019-11-29T15:25:56+01:00 | ||
a680930 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8 | 6 | 2019-12-07T12:18:41+01:00 | ||
7832e15 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 6 | 2019-12-01T00:31:58+01:00 | ||
4e2930c | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-04T01:26 CET (comp) |
Found 28 witnesses for program sv-benchmarks/c/ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i, 581839242835660c7049651d3b011957f2644fd34c14926011425d9d7608c10b
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/581839242835660c7049651d3b011957f2644fd34c14926011425d9d7608c10b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
70bbabb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T17:25 CET (sv-comp) | ||
57fb7c8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 3 | 2018-12-08T16:03:56 | ||
bb683f6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 5 | 2018-12-07T04:11 CET (sv-comp) | ||
9e8584e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 6 | 2018-12-10T17:17:47+01:00 | ||
80a2336 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 6 | 2018-12-06T23:03:36+01:00 | ||
68cd2b2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-10T20:34:49+01:00 | 9e8584e | |
e83a2a3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-10T10:48:52+01:00 | 6d6f113 | |
90585d5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-09T20:53:09+01:00 | 90c3071 | |
54131bf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-09T20:37:42+01:00 | 92f7f8c | |
4aae08f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-09T20:19:08+01:00 | a48e9ff | |
734503b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-09T17:55:32+01:00 | b74f1c0 | |
391d825 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T23:42:59+01:00 | 70bbabb | |
14ed281 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T22:08:57+01:00 | 57fb7c8 | |
621b127 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T08:47:55+01:00 | 80a2336 | |
75786b0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T05:02:54+01:00 | 12c07c8 | |
4a93456 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T04:11:55+01:00 | 6d6f113 | |
a83da58 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-07T18:47:52+01:00 | cb3bab8 | |
02d8a75 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-07T09:29:49+01:00 | 1bdebff | |
e4763f3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-07T01:16:32+01:00 | 135ab70 | |
55fb0f6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T10:18:26+01:00 | c367be0 | |
b6e1382 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T09:48:09+01:00 | 7cfbcfe | |
9cc6bc5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T09:41:41+01:00 | b77f397 | |
7cfbcfe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-05T11:59:00+01:00 | ||
8e4a749 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-07T17:44:18+01:00 | bb683f6 | |
d06e432 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:18:00+01:00 | 592ee0f | |
e919969 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:17:00+01:00 | 73d07ae | |
437fd32 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T11:37 CET (sv-comp) | ||
228ccbd | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T15:39 CET (sv-comp) |
Found 23 witnesses for program sv-benchmarks/c/ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i, 581839242835660c7049651d3b011957f2644fd34c14926011425d9d7608c10b
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/581839242835660c7049651d3b011957f2644fd34c14926011425d9d7608c10b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
03c7ff8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | skink | 3 | 2017-12-01T23:44 CET (sv-comp) | ||
e08502f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 6 | 2017-12-02T21:12Z | ||
abd6b1a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T00:14 CET (sv-comp) | ||
1bdebff | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | PredatorHP | 4 | 2017-12-01T20:36 CET (sv-comp) | ||
f39ce16 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Map2Check | 3 | 2017-12-01T20:34 CET (sv-comp) | ||
c90b650 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 6 | 2017-12-02T09:14Z | ||
5825ec0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Forester | 5 | 2017-12-01T17:55 CET (sv-comp) | ||
795a29b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-01T20:25:12.671942 | ||
df00030 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T15:42:54.773825 | ||
ed7a60f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 4 | 2017-12-01T20:19 CET (sv-comp) | ||
25666dc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 4 | 2017-12-01T06:46 CET (sv-comp) | ||
6a939de | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn | 6 | 2017-12-02T19:32:09+01:00 | ||
97d8d9b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-01T01:25:18+01:00 | ||
4405e4f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 8 | 2017-11-30T21:02:04+01:00 | ||
2a6de81 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 5 | 2017-11-30T19:11:39+01:00 | ||
aa3bc35 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 7 | 2017-12-02T08:23:17+01:00 | ||
6484f21 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 5 | 2017-11-30T23:43 CET (sv-comp) | ||
0ee9bf3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 6 | 2017-12-02T17:00Z | ||
0f1daa3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 4 | 2017-11-30T18:23 CET (sv-comp) | ||
10bff04 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-03T00:27:38.941624 | ||
8201b22 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T12:25:41.865083 | ||
96f3851 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 5 | 2017-12-01T14:43 CET (sv-comp) | ||
498e591 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 10 | 2017-12-01T12:28 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i, 581839242835660c7049651d3b011957f2644fd34c14926011425d9d7608c10b
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/581839242835660c7049651d3b011957f2644fd34c14926011425d9d7608c10b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |