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/locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c |
programSHA | 118c4c3947bd3ab94d28b710cca3e8cdaaf2fe60d2fb1dda9eb0ae218fbf0425 |
witnessName | results-validated/cpa-seq-validate-correctness-witnesses-uautomizer.2018-12-09_1643.logfiles/sv-comp19_prop-reachsafety.test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c.files/witness.graphml |
witnessSHA | 7473a501640b849844022239c9c4d81822ea2ed3bac51dc17e96ac66bdedf73d |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-09T17:36:40+01:00 |
inputwitnesshash | a393aeb1a4ea45afb792d27a6e34d854fc80ff65b90d26a5c2c77b866c13a850 |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | 118c4c3947bd3ab94d28b710cca3e8cdaaf2fe60d2fb1dda9eb0ae218fbf0425 |
programfile | ../../sv-benchmarks/c/locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c |
programhash | 118c4c3947bd3ab94d28b710cca3e8cdaaf2fe60d2fb1dda9eb0ae218fbf0425 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/7473a501640b849844022239c9c4d81822ea2ed3bac51dc17e96ac66bdedf73d.graphml |
witness-sha256 | 7473a501640b849844022239c9c4d81822ea2ed3bac51dc17e96ac66bdedf73d |
witness-size | 13196 |
witness-type | correctness_witness |
This witness was created for this program (cf. table above, 118c4c3947bd3ab94d28b710cca3e8cdaaf2fe60d2fb1dda9eb0ae218fbf0425).
Found 0 witnesses for program sv-benchmarks/c/locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c, 118c4c3947bd3ab94d28b710cca3e8cdaaf2fe60d2fb1dda9eb0ae218fbf0425
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/118c4c3947bd3ab94d28b710cca3e8cdaaf2fe60d2fb1dda9eb0ae218fbf0425.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c, 118c4c3947bd3ab94d28b710cca3e8cdaaf2fe60d2fb1dda9eb0ae218fbf0425
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/118c4c3947bd3ab94d28b710cca3e8cdaaf2fe60d2fb1dda9eb0ae218fbf0425.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c, 118c4c3947bd3ab94d28b710cca3e8cdaaf2fe60d2fb1dda9eb0ae218fbf0425
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/118c4c3947bd3ab94d28b710cca3e8cdaaf2fe60d2fb1dda9eb0ae218fbf0425.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c, 118c4c3947bd3ab94d28b710cca3e8cdaaf2fe60d2fb1dda9eb0ae218fbf0425
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/118c4c3947bd3ab94d28b710cca3e8cdaaf2fe60d2fb1dda9eb0ae218fbf0425.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 15 witnesses for program sv-benchmarks/c/locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c, 118c4c3947bd3ab94d28b710cca3e8cdaaf2fe60d2fb1dda9eb0ae218fbf0425
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/118c4c3947bd3ab94d28b710cca3e8cdaaf2fe60d2fb1dda9eb0ae218fbf0425.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ccba283 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 13 | 2019-11-30T20:57:02+01:00 | ||
ad23d07 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.9 | 13 | 2019-11-29T19:27:24+01:00 | ||
4aa89a4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-11T20:31:05+01:00 | 050ee13 | |
a9fc5f8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-11T20:16:34+01:00 | ea6feee | |
9aa7d5b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-11T20:02:57+01:00 | 8cc7a69 | |
ac6ef09 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-08T00:36:32+01:00 | 0188866 | |
76a1816 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-07T23:33:18+01:00 | 6a9c48c | |
5acddf8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-07T19:45:20+01:00 | 6ff9227 | |
81f2722 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-05T19:02:51+01:00 | 454a2ea | |
b6a61f3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-11-30T17:12:01+01:00 | ca64642 | |
ca64642 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 13 | 2019-11-30T14:54:27+01:00 | ||
0188866 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8 | 13 | 2019-12-07T12:24:42+01:00 | ||
ea6feee | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 13 | 2019-12-01T10:21:19+01:00 | ||
1d14616 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.9 | 22 | 2019-11-30T12:04:23+01:00 | ||
bedc61b | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 22 | 2019-12-01T00:16:41+01:00 |
Found 22 witnesses for program sv-benchmarks/c/locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c, 118c4c3947bd3ab94d28b710cca3e8cdaaf2fe60d2fb1dda9eb0ae218fbf0425
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/118c4c3947bd3ab94d28b710cca3e8cdaaf2fe60d2fb1dda9eb0ae218fbf0425.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
03a9857 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T09:45 CET (sv-comp) | ||
b2d823f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 13 | 2018-12-07T10:04:37+01:00 | ||
2c4a885 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-05T20:09:38+01:00 | ||
1a712d1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T01:53 CET (sv-comp) | ||
1181718 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T07:27:58 | ||
ab0d5a0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 13 | 2018-12-07T03:11:57+01:00 | ||
ba568ab | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-10T19:55:23+01:00 | e626b8b | |
87b39f6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-09T20:29:53+01:00 | 0975250 | |
aadb717 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-09T19:50:22+01:00 | 9b2d601 | |
7473a50 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-09T17:36:40+01:00 | a393aeb | |
1a92ef1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T23:10:05+01:00 | 1a712d1 | |
a5edcfe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T21:41:23+01:00 | 1181718 | |
897e048 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T06:00:17+01:00 | ab0d5a0 | |
d752a0d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T03:58:41+01:00 | fef2b91 | |
241a8a4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-07T17:43:03+01:00 | 39f01d9 | |
258d683 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-06T09:28:16+01:00 | 4823b38 | |
1b912d6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-06T09:01:16+01:00 | cd02a49 | |
a59b801 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-06T08:15:08+01:00 | 1ee0243 | |
cd02a49 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-05T10:26:21+01:00 | ||
35226c6 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 22 | 2018-12-07T20:40:46+01:00 | ||
29c7cff | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-09T20:39:00+01:00 | ||
2491bef | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-05T19:54:47+01:00 |
Found 37 witnesses for program sv-benchmarks/c/locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c, 118c4c3947bd3ab94d28b710cca3e8cdaaf2fe60d2fb1dda9eb0ae218fbf0425
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/118c4c3947bd3ab94d28b710cca3e8cdaaf2fe60d2fb1dda9eb0ae218fbf0425.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
42a404a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T23:11 CET (sv-comp) | ||
9f011ca | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T11:44:29.167114 | ||
82a3d80 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 3.1 | 28 | 2017-12-01T09:32 CET (sv-comp) | ||
f684beb | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Taipan | 19 | 2017-12-03T06:53Z | ||
e4ec674 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Kojak | 20 | 2017-12-03T04:08Z | ||
dc3a397 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Automizer | 19 | 2017-12-03T04:14Z | ||
e2fdc4a | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | 2LS | 30 | 2017-12-01T08:25 CET (sv-comp) | ||
39f01d9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | skink | 3 | 2017-12-01T22:12 CET (sv-comp) | ||
1c98454 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Taipan | 20 | 2017-12-03T03:37Z | ||
9baa3eb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T15:09 CET (sv-comp) | ||
347344d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Kojak | 20 | 2017-12-02T07:19Z | ||
8e6f1aa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-01T19:13:50.301347 | ||
9450d8f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 28 | 2017-12-01T20:51 CET (sv-comp) | ||
8021955 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 14 | 2017-12-03T00:57:16+01:00 | ||
2aecc43 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-11-30T16:54:15+01:00 | ||
8b14286 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-03T07:06:00+01:00 | 4766f9e | |
ddfb61a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 14 | 2017-12-03T04:18:09+01:00 | e78e749 | |
b5db7d9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-03T01:05:15+01:00 | f381d52 | |
a530b9d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-02T23:59:11+01:00 | 40c35f7 | |
c9dd11a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-02T19:56:11+01:00 | 3535557 | |
5370c69 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-02T14:40:42+01:00 | 96d44ed | |
139bb42 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-02T08:14:27+01:00 | 83b922c | |
681355b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-02T00:16:52+01:00 | 58063aa | |
69d46cc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-01T08:14:09+01:00 | 93fa885 | |
bdba61c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-01T07:04:29+01:00 | b5038af | |
78fdb0f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-01T07:01:57+01:00 | 97ea293 | |
7ff844a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-01T06:56:40+01:00 | 203dd50 | |
d74cb93 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-01T05:01:57+01:00 | 80bbce8 | |
4819d07 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-01T02:38:59+01:00 | ||
62a7fb1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 15 | 2017-11-30T12:14:22+01:00 | ||
459d059 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26725 | 13 | 2017-11-30T20:15:47+01:00 | ||
9e0d9a7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker (unknown version) | 13 | 2017-12-02T06:02:58+01:00 | ||
9c9b5d8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 20 | 2017-12-02T08:48Z | ||
549c24f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 30 | 2017-11-30T12:30 CET (sv-comp) | ||
7cc8f6d | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 22 | 2017-12-01T14:21:50+01:00 | ||
75e51d2 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Automizer | 16 | 2017-12-03T11:14Z | ||
3466d83 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 13 | 2017-12-01T11:51 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c, 118c4c3947bd3ab94d28b710cca3e8cdaaf2fe60d2fb1dda9eb0ae218fbf0425
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/118c4c3947bd3ab94d28b710cca3e8cdaaf2fe60d2fb1dda9eb0ae218fbf0425.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |