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).
Found 0 witnesses for program sv-benchmarks/c/locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c, 38012c6fd9010b95cb453d061d6d78724cf269ace5309358f8dab44ee4ab3afe
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/38012c6fd9010b95cb453d061d6d78724cf269ace5309358f8dab44ee4ab3afe.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_15_true-unreach-call_true-valid-memsafety_false-termination.c, 38012c6fd9010b95cb453d061d6d78724cf269ace5309358f8dab44ee4ab3afe
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/38012c6fd9010b95cb453d061d6d78724cf269ace5309358f8dab44ee4ab3afe.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_15_true-unreach-call_true-valid-memsafety_false-termination.c, 38012c6fd9010b95cb453d061d6d78724cf269ace5309358f8dab44ee4ab3afe
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/38012c6fd9010b95cb453d061d6d78724cf269ace5309358f8dab44ee4ab3afe.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_15_true-unreach-call_true-valid-memsafety_false-termination.c, 38012c6fd9010b95cb453d061d6d78724cf269ace5309358f8dab44ee4ab3afe
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/38012c6fd9010b95cb453d061d6d78724cf269ace5309358f8dab44ee4ab3afe.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_15_true-unreach-call_true-valid-memsafety_false-termination.c, 38012c6fd9010b95cb453d061d6d78724cf269ace5309358f8dab44ee4ab3afe
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/38012c6fd9010b95cb453d061d6d78724cf269ace5309358f8dab44ee4ab3afe.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
2c4e9cc | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.9 | 27 | 2019-11-29T17:07:50+01:00 | ||
7b9d32c | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 27 | 2019-11-30T21:27:10+01:00 | ||
4044857 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 27 | 2019-12-11T20:30:35+01:00 | 899e361 | |
5e1e999 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 27 | 2019-12-11T20:21:34+01:00 | b56a4dc | |
303eb56 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 27 | 2019-12-11T20:02:17+01:00 | 1ac0372 | |
993ea88 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 27 | 2019-12-08T00:50:49+01:00 | af079ae | |
c6700b8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 27 | 2019-12-07T23:15:41+01:00 | 15ba6e9 | |
3fe6ff3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 27 | 2019-12-07T19:47:23+01:00 | 37b44bd | |
9b17f32 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 27 | 2019-12-05T19:02:54+01:00 | 8acc3f3 | |
0fc6a45 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 27 | 2019-11-30T16:53:49+01:00 | 7aff0b0 | |
7aff0b0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 27 | 2019-11-29T16:28:13+01:00 | ||
af079ae | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8 | 27 | 2019-12-07T22:31:01+01:00 | ||
b56a4dc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 27 | 2019-12-01T19:27:03+01:00 | ||
0fb8fc8 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.9 | 50 | 2019-11-30T09:35:37+01:00 | ||
5d04010 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 50 | 2019-11-30T22:55:53+01:00 |
Found 22 witnesses for program sv-benchmarks/c/locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c, 38012c6fd9010b95cb453d061d6d78724cf269ace5309358f8dab44ee4ab3afe
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/38012c6fd9010b95cb453d061d6d78724cf269ace5309358f8dab44ee4ab3afe.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
2cc3cdc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T02:23 CET (sv-comp) | ||
6cc1304 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 27 | 2018-12-07T09:53:09+01:00 | ||
aafb448 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-06T07:06:52+01:00 | ||
59b1da5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T17:19 CET (sv-comp) | ||
2a5a7cb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T04:04:24 | ||
152ec56 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7 | 27 | 2018-12-10T19:05:15+01:00 | ||
6defc18 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 27 | 2018-12-08T03:54:26+01:00 | ||
270144d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-10T19:40:54+01:00 | 152ec56 | |
183b826 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-09T20:33:35+01:00 | 5c3a530 | |
f9d310b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-09T19:48:12+01:00 | f23a324 | |
ed82caf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-09T17:13:57+01:00 | 8bbb3b2 | |
6c2a1ef | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-08T23:14:15+01:00 | 59b1da5 | |
5aecc09 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-08T21:46:09+01:00 | 2a5a7cb | |
4f67a0f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-08T07:12:06+01:00 | 6defc18 | |
7d4d83a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-08T03:26:39+01:00 | 2dac678 | |
094d2c4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-07T17:32:28+01:00 | aa5c53c | |
889c74c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-06T09:28:38+01:00 | 71e65e3 | |
5807391 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-06T09:14:57+01:00 | 5b0d7ac | |
3adb0d4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-06T08:08:36+01:00 | 8b007c4 | |
5b0d7ac | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-06T06:54:14+01:00 | ||
5ebdb9a | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 49 | 2018-12-08T00:54:58+01:00 | ||
88aca20 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 50 | 2018-12-05T22:55:42+01:00 |
Found 35 witnesses for program sv-benchmarks/c/locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c, 38012c6fd9010b95cb453d061d6d78724cf269ace5309358f8dab44ee4ab3afe
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/38012c6fd9010b95cb453d061d6d78724cf269ace5309358f8dab44ee4ab3afe.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
2a2136b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2017-12-03T00:22 CET (sv-comp) | ||
cae36b1 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T11:55:14.139310 | ||
aabec41 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 3.1 | 94 | 2017-12-01T09:42 CET (sv-comp) | ||
a3366da | 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 | 42 | 2017-12-03T06:53Z | ||
546a3e6 | 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 | 44 | 2017-12-03T03:54Z | ||
aba580f | 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 | 42 | 2017-12-03T04:11Z | ||
4d91609 | 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 | 66 | 2017-12-01T08:21 CET (sv-comp) | ||
aa5c53c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | skink | 3 | 2017-12-01T23:51 CET (sv-comp) | ||
21e8158 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Taipan | 43 | 2017-12-03T01:43Z | ||
efe097b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T07:39 CET (sv-comp) | ||
f4b940a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Kojak | 44 | 2017-12-02T14:15Z | ||
6117248 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-01T21:19:47.839788 | ||
e0d4f0d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 95 | 2017-12-01T17:58 CET (sv-comp) | ||
b3ca8af | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 28 | 2017-12-02T19:48:55+01:00 | ||
0e5c407 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-12-01T01:06:55+01:00 | ||
245efd9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 27 | 2017-12-03T06:51:24+01:00 | 8da4711 | |
b7b029c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 28 | 2017-12-03T04:15:19+01:00 | 97cb424 | |
4ead34b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 27 | 2017-12-03T02:42:09+01:00 | ec53003 | |
216ba82 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 27 | 2017-12-03T01:38:03+01:00 | bc9147e | |
177a7b1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 27 | 2017-12-02T20:33:06+01:00 | 15b062f | |
af1f3cf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 27 | 2017-12-02T08:56:10+01:00 | fc9218f | |
77f0605 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 27 | 2017-12-02T00:16:19+01:00 | 1554e1e | |
0ea1937 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 27 | 2017-12-01T08:14:05+01:00 | c7ef5c5 | |
5b1a5b4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 27 | 2017-12-01T06:18:06+01:00 | 1d42ff4 | |
09ae931 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 27 | 2017-12-01T05:27:45+01:00 | 3ca5b5e | |
4fc8f26 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 27 | 2017-12-01T05:17:14+01:00 | 2523d4c | |
6bcba6c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 27 | 2017-12-01T04:55:12+01:00 | 6f077b1 | |
8205e6c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 27 | 2017-11-30T13:57:21+01:00 | ||
fa71a4d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 28 | 2017-12-01T01:02:20+01:00 | ||
75c220d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26725 | 27 | 2017-11-30T14:56:16+01:00 | ||
689bce9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 43 | 2017-12-02T02:50Z | ||
ab36303 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 66 | 2017-11-30T18:16 CET (sv-comp) | ||
fe8b8df | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 49 | 2017-12-01T16:31:15+01:00 | ||
6b84ef5 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Automizer | 34 | 2017-12-03T11:14Z | ||
91d9381 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 27 | 2017-12-01T13:36 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c, 38012c6fd9010b95cb453d061d6d78724cf269ace5309358f8dab44ee4ab3afe
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/38012c6fd9010b95cb453d061d6d78724cf269ace5309358f8dab44ee4ab3afe.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |