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_7_true-unreach-call_true-valid-memsafety_false-termination.c |
programSHA | 960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa |
witnessName | results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c.files/witness.graphml |
witnessSHA | d12da80612ebf08da676a54eace80882b4b0ecdd405c15680fa63cd0c1644690 |
Key | Value |
architecture | 32bit |
creationtime | 2017-11-30T11:41 CET (sv-comp) |
producer | 2LS |
program-sha256 | 960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa |
programfile | ../../sv-benchmarks/c/locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c |
programhash | ccd6d122756047ddb1225c106ac06a6748e14c22 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/d12da80612ebf08da676a54eace80882b4b0ecdd405c15680fa63cd0c1644690.graphml |
witness-sha256 | d12da80612ebf08da676a54eace80882b4b0ecdd405c15680fa63cd0c1644690 |
witness-size | 34018 |
witness-type | correctness_witness |
Found 0 witnesses for program sv-benchmarks/c/locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c, 960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa.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_7_true-unreach-call_true-valid-memsafety_false-termination.c, 960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa.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_7_true-unreach-call_true-valid-memsafety_false-termination.c, 960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa.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_7_true-unreach-call_true-valid-memsafety_false-termination.c, 960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa.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_7_true-unreach-call_true-valid-memsafety_false-termination.c, 960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
40273a9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 15 | 2019-11-29T17:12:28+01:00 | ||
b903787 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 15 | 2019-11-30T21:14:49+01:00 | ||
182fc8e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 15 | 2019-12-11T20:22:37+01:00 | 49a6e9c | |
0a7eea2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 15 | 2019-12-11T20:17:28+01:00 | a023968 | |
e28cc75 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 15 | 2019-12-11T20:02:18+01:00 | 2069709 | |
eb8c1fc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 15 | 2019-12-08T00:39:58+01:00 | a637597 | |
1c59f39 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 15 | 2019-12-07T23:45:29+01:00 | 9b7f621 | |
a8df326 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 15 | 2019-12-07T19:45:37+01:00 | 5b69b63 | |
1818005 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 15 | 2019-12-05T19:02:50+01:00 | 2606d84 | |
b3149bf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 15 | 2019-11-30T17:14:28+01:00 | 0aa04b7 | |
0aa04b7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 15 | 2019-11-30T02:34:53+01:00 | ||
a637597 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8 | 15 | 2019-12-07T14:35:13+01:00 | ||
a023968 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 15 | 2019-11-30T22:54:35+01:00 | ||
d2101fe | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.9 | 25 | 2019-11-29T16:45:41+01:00 | ||
b571bdb | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 25 | 2019-12-01T00:00:59+01:00 |
Found 23 witnesses for program sv-benchmarks/c/locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c, 960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
fd3d6dc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T08:34 CET (sv-comp) | ||
2b181f3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-05T15:47:02+01:00 | ||
204fa53 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 15 | 2018-12-08T03:17:33+01:00 | ||
04a8135 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T10:39 CET (sv-comp) | ||
a10c749 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T16:43:46 | ||
b63c782 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 15 | 2018-12-06T21:25:40+01:00 | ||
2d1428b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-10T20:08:05+01:00 | 068ad9b | |
d6d3612 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-09T20:14:31+01:00 | cd43580 | |
bac139a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-09T19:53:00+01:00 | 3c9c1b4 | |
c278f92 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-09T17:13:06+01:00 | 9a25083 | |
111f514 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-08T23:09:47+01:00 | 04a8135 | |
6d796bd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-08T21:38:22+01:00 | a10c749 | |
ca4e277 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-08T06:28:31+01:00 | b63c782 | |
a0ff806 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-08T03:48:08+01:00 | 064913a | |
87c6652 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-07T17:45:12+01:00 | bb0db58 | |
80b2bad | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-06T09:28:47+01:00 | 281ecb4 | |
7497dec | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-06T08:52:31+01:00 | 5baebe2 | |
5baebe2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-06T07:49:51+01:00 | ||
1b5a919 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-06T07:41:48+01:00 | 1766138 | |
4bc2d9d | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 25 | 2018-12-07T05:53:41+01:00 | ||
d823ff0 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 23 | 2018-12-09T20:34:31+01:00 | ||
dfce4f2 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 26 | 2018-12-06T09:41:41+01:00 | ||
0fffcdb | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 25 | 2018-12-06T07:49:15+01:00 |
Found 37 witnesses for program sv-benchmarks/c/locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c, 960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
96f88a7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2017-12-03T00:19 CET (sv-comp) | ||
ff9e5a9 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T11:13:02.365524 | ||
1570c8d | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 3.1 | 33 | 2017-12-01T09:16 CET (sv-comp) | ||
30e3fd3 | 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 | 22 | 2017-12-03T06:53Z | ||
1b048e6 | 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 | 23 | 2017-12-03T04:07Z | ||
f84eae7 | 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 | 22 | 2017-12-03T03:43Z | ||
da2096b | 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 | 34 | 2017-12-01T08:21 CET (sv-comp) | ||
bb0db58 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | skink | 3 | 2017-12-01T22:26 CET (sv-comp) | ||
5a6e192 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Taipan | 22 | 2017-12-03T02:39Z | ||
a633f6c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T00:04 CET (sv-comp) | ||
1a6355b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Kojak | 23 | 2017-12-02T12:50Z | ||
9cf329a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-01T19:45:58.248002 | ||
ee1be48 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 33 | 2017-12-01T17:11 CET (sv-comp) | ||
dc93d52 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 15 | 2017-12-02T21:20:35+01:00 | ||
8c0bc5e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-11-30T17:40:39+01:00 | ||
093f187 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 15 | 2017-12-03T07:03:54+01:00 | fb1f688 | |
5f3b758 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 15 | 2017-12-03T04:26:21+01:00 | 7764d1d | |
f7c5956 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 15 | 2017-12-03T02:35:04+01:00 | 4e9687b | |
4c63d50 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 15 | 2017-12-03T01:54:49+01:00 | a11034a | |
49f458c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 15 | 2017-12-02T20:09:10+01:00 | 4ae75f3 | |
c140b6d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 15 | 2017-12-02T14:49:53+01:00 | 0582873 | |
19141b0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 15 | 2017-12-02T08:37:06+01:00 | 217aab7 | |
37316ed | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 15 | 2017-12-02T00:09:03+01:00 | 9ba1390 | |
bec8121 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 15 | 2017-12-01T08:13:56+01:00 | bddf76b | |
2fc21d9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 15 | 2017-12-01T06:23:08+01:00 | f4b33a1 | |
a2ffb61 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 15 | 2017-12-01T05:39:11+01:00 | ef6a8d0 | |
9466a0d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 15 | 2017-12-01T04:55:44+01:00 | 2efec5c | |
161fee2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 15 | 2017-12-01T04:35:11+01:00 | 05298f3 | |
883f70a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 15 | 2017-12-01T01:59:14+01:00 | ||
7a89b67 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 16 | 2017-12-01T00:18:32+01:00 | ||
f695dd7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26725 | 15 | 2017-11-30T17:58:04+01:00 | ||
a15f96e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker (unknown version) | 14 | 2017-12-01T19:12:35+01:00 | ||
61c645a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 22 | 2017-12-02T04:59Z | ||
d12da80 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 34 | 2017-11-30T11:41 CET (sv-comp) | ||
d1f1df8 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 25 | 2017-12-01T14:43:59+01:00 | ||
ecb4982 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Automizer | 18 | 2017-12-03T11:12Z | ||
a78ac71 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 15 | 2017-12-01T13:50 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c, 960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/960ebe4d3c4102c70b7edeef48a711d6c5b3fd34f5f7c1bdd9c01e16774d27aa.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |