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_9_true-unreach-call_true-valid-memsafety_false-termination.c |
programSHA | b00c421a75b9aed50d723fd66635e08da87aefa05a25b77d2811f84f1d8eb31e |
witnessName | results-verified/ukojak.2017-12-03_0440.logfiles/sv-comp18.test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c.files/witness.graphml |
witnessSHA | 479e617a62b0cca63a575afc854334260bff1156bd710ebfd9e31045f72cf585 |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-03T04:17Z |
error-specification-length | Key 'specification' longer than 100 characters. |
producer | Kojak |
program-sha256 | b00c421a75b9aed50d723fd66635e08da87aefa05a25b77d2811f84f1d8eb31e |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_a81fe05c-b1f6-43ed-ae73-9954657c0b8f/sv-benchmarks/c/locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c |
programhash | 5107685577f81a5867811396b2c0a05eb5630c95 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) |
witness-file | witnessFileByHash/479e617a62b0cca63a575afc854334260bff1156bd710ebfd9e31045f72cf585.graphml |
witness-sha256 | 479e617a62b0cca63a575afc854334260bff1156bd710ebfd9e31045f72cf585 |
witness-size | 28098 |
witness-type | correctness_witness |
Found 0 witnesses for program sv-benchmarks/c/locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c, b00c421a75b9aed50d723fd66635e08da87aefa05a25b77d2811f84f1d8eb31e
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/b00c421a75b9aed50d723fd66635e08da87aefa05a25b77d2811f84f1d8eb31e.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_9_true-unreach-call_true-valid-memsafety_false-termination.c, b00c421a75b9aed50d723fd66635e08da87aefa05a25b77d2811f84f1d8eb31e
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/b00c421a75b9aed50d723fd66635e08da87aefa05a25b77d2811f84f1d8eb31e.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_9_true-unreach-call_true-valid-memsafety_false-termination.c, b00c421a75b9aed50d723fd66635e08da87aefa05a25b77d2811f84f1d8eb31e
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/b00c421a75b9aed50d723fd66635e08da87aefa05a25b77d2811f84f1d8eb31e.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_9_true-unreach-call_true-valid-memsafety_false-termination.c, b00c421a75b9aed50d723fd66635e08da87aefa05a25b77d2811f84f1d8eb31e
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/b00c421a75b9aed50d723fd66635e08da87aefa05a25b77d2811f84f1d8eb31e.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_9_true-unreach-call_true-valid-memsafety_false-termination.c, b00c421a75b9aed50d723fd66635e08da87aefa05a25b77d2811f84f1d8eb31e
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/b00c421a75b9aed50d723fd66635e08da87aefa05a25b77d2811f84f1d8eb31e.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ece9dbc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 18 | 2019-11-30T14:01:51+01:00 | ||
fda7f3a | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 18 | 2019-12-01T16:48:34+01:00 | ||
956b3e1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 18 | 2019-12-11T20:31:05+01:00 | 54f4df1 | |
93008af | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 18 | 2019-12-11T20:17:41+01:00 | 8bff675 | |
32f65c6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 18 | 2019-12-11T20:02:51+01:00 | 5cb29f1 | |
c90399e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 18 | 2019-12-08T00:59:43+01:00 | e770d47 | |
c351426 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 18 | 2019-12-07T23:43:51+01:00 | 9160646 | |
9a36da2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 18 | 2019-12-07T19:45:33+01:00 | 5de5f7c | |
92a87ed | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 18 | 2019-12-05T19:03:03+01:00 | b108843 | |
fb5ae44 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 18 | 2019-11-30T17:11:58+01:00 | c7df4dc | |
c7df4dc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 18 | 2019-11-29T14:04:45+01:00 | ||
e770d47 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8 | 18 | 2019-12-07T20:20:49+01:00 | ||
8bff675 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 18 | 2019-12-01T16:25:03+01:00 | ||
42f2aca | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.9 | 31 | 2019-11-30T02:59:57+01:00 | ||
783f226 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 31 | 2019-12-01T18:20:48+01:00 |
Found 22 witnesses for program sv-benchmarks/c/locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c, b00c421a75b9aed50d723fd66635e08da87aefa05a25b77d2811f84f1d8eb31e
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/b00c421a75b9aed50d723fd66635e08da87aefa05a25b77d2811f84f1d8eb31e.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
73c662e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T03:26 CET (sv-comp) | ||
c1cb753 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 18 | 2018-12-06T05:37:25+01:00 | ||
41ffcf8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T05:53 CET (sv-comp) | ||
ee8d011 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T03:18:47 | ||
1f3a3b1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 18 | 2018-12-07T20:36:18+01:00 | ||
d3c9cff | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 18 | 2018-12-10T20:00:56+01:00 | 497a4b2 | |
f621dfb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 18 | 2018-12-09T20:33:18+01:00 | 3bbb462 | |
c1dd144 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 18 | 2018-12-09T20:01:44+01:00 | da951b7 | |
5e7711e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 18 | 2018-12-09T19:54:09+01:00 | f98b178 | |
d12c921 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 18 | 2018-12-08T23:09:32+01:00 | 41ffcf8 | |
90c5ef8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 18 | 2018-12-08T20:53:14+01:00 | ee8d011 | |
525db83 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 18 | 2018-12-08T05:16:07+01:00 | 1f3a3b1 | |
d83c911 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 18 | 2018-12-08T02:56:11+01:00 | e3b19ec | |
697b4c1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 18 | 2018-12-07T17:45:12+01:00 | 9794e5e | |
1229296 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 18 | 2018-12-06T09:28:45+01:00 | 422dad4 | |
85245fc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 18 | 2018-12-06T08:45:29+01:00 | 6d051e9 | |
047c9aa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 18 | 2018-12-06T07:04:33+01:00 | 2020e18 | |
6d051e9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 18 | 2018-12-06T02:22:30+01:00 | ||
d691fe4 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 31 | 2018-12-08T04:08:22+01:00 | ||
5ee5b70 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 28 | 2018-12-09T20:39:16+01:00 | ||
db0be76 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 33 | 2018-12-06T09:40:44+01:00 | ||
916f565 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 31 | 2018-12-05T11:24:58+01:00 |
Found 37 witnesses for program sv-benchmarks/c/locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c, b00c421a75b9aed50d723fd66635e08da87aefa05a25b77d2811f84f1d8eb31e
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/b00c421a75b9aed50d723fd66635e08da87aefa05a25b77d2811f84f1d8eb31e.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
d03ab46 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T23:51 CET (sv-comp) | ||
008fa05 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T10:52:29.691716 | ||
cb0535e | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 3.1 | 46 | 2017-12-01T09:22 CET (sv-comp) | ||
2ec90da | 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 | 27 | 2017-12-03T06:53Z | ||
479e617 | 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 | 28 | 2017-12-03T04:17Z | ||
e586b69 | 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 | 27 | 2017-12-03T03:43Z | ||
7870a11 | 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 | 42 | 2017-12-01T08:25 CET (sv-comp) | ||
9794e5e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | skink | 3 | 2017-12-01T23:53 CET (sv-comp) | ||
11b7b2e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Taipan | 27 | 2017-12-03T02:57Z | ||
2df993c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T18:38 CET (sv-comp) | ||
626a928 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Kojak | 28 | 2017-12-02T08:11Z | ||
39deb6d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-01T16:52:37.546160 | ||
c7478f6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 46 | 2017-12-01T17:19 CET (sv-comp) | ||
3f54f24 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 18 | 2017-12-02T20:47:36+01:00 | ||
d69670a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-12-01T05:31:11+01:00 | ||
3388998 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 18 | 2017-12-03T06:59:32+01:00 | c3a6ce3 | |
e5f3e8b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 18 | 2017-12-03T04:18:27+01:00 | 76e652c | |
8413150 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 18 | 2017-12-03T02:59:48+01:00 | 65e45bd | |
5b10ced | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 18 | 2017-12-03T00:46:02+01:00 | 5b162df | |
ecff49f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 18 | 2017-12-02T20:10:14+01:00 | 9fa517d | |
b7d0259 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 18 | 2017-12-02T15:21:43+01:00 | fea5cbb | |
1dd785c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 18 | 2017-12-02T09:01:19+01:00 | 194323d | |
1f535cf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 18 | 2017-12-02T00:04:28+01:00 | 59bfdfc | |
c56ba93 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 18 | 2017-12-01T08:13:09+01:00 | 5b68a18 | |
6b6dfeb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 18 | 2017-12-01T07:01:55+01:00 | 692a9ab | |
fa7b0b4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 18 | 2017-12-01T06:23:01+01:00 | 52e28d2 | |
367ccfa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 18 | 2017-12-01T06:15:01+01:00 | ea844be | |
925c9fe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 18 | 2017-12-01T05:27:41+01:00 | 6168067 | |
da0d2ff | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 18 | 2017-11-30T20:21:31+01:00 | ||
3bc512d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 19 | 2017-12-01T02:26:16+01:00 | ||
4967dd7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26725 | 18 | 2017-11-30T17:59:33+01:00 | ||
b99045f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker (unknown version) | 17 | 2017-12-01T19:53:32+01:00 | ||
55f5000 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 27 | 2017-12-02T02:41Z | ||
0151b7c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 42 | 2017-11-30T15:32 CET (sv-comp) | ||
a35a70d | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 31 | 2017-12-01T13:52:40+01:00 | ||
15ed721 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Automizer | 22 | 2017-12-03T11:13Z | ||
26e7efa | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 18 | 2017-12-01T12:29 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c, b00c421a75b9aed50d723fd66635e08da87aefa05a25b77d2811f84f1d8eb31e
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/b00c421a75b9aed50d723fd66635e08da87aefa05a25b77d2811f84f1d8eb31e.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |