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_14_false-unreach-call_true-valid-memsafety_false-termination.c |
programSHA | a3e8e2f2e732e3d055a8530bee1dde0ce1d9b0781c95b8d367dc12736fc0ac3f |
witnessName | results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c.files/witness.graphml |
witnessSHA | c3619bc6f9b8f2dcc2cea2640da25e115a353ebee502e37d1666d9a0b9b871d9 |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-01T03:44:43+01:00 |
producer | CPAchecker 1.6.1-svn 26773 |
program-sha256 | a3e8e2f2e732e3d055a8530bee1dde0ce1d9b0781c95b8d367dc12736fc0ac3f |
programfile | ../../sv-benchmarks/c/locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c |
programhash | 4c4a63b42b00dbfea9a5b040626d99ec84a4e61b |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/c3619bc6f9b8f2dcc2cea2640da25e115a353ebee502e37d1666d9a0b9b871d9.graphml |
witness-sha256 | c3619bc6f9b8f2dcc2cea2640da25e115a353ebee502e37d1666d9a0b9b871d9 |
witness-size | 19312 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c, a3e8e2f2e732e3d055a8530bee1dde0ce1d9b0781c95b8d367dc12736fc0ac3f
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/a3e8e2f2e732e3d055a8530bee1dde0ce1d9b0781c95b8d367dc12736fc0ac3f.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_14_false-unreach-call_true-valid-memsafety_false-termination.c, a3e8e2f2e732e3d055a8530bee1dde0ce1d9b0781c95b8d367dc12736fc0ac3f
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/a3e8e2f2e732e3d055a8530bee1dde0ce1d9b0781c95b8d367dc12736fc0ac3f.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_14_false-unreach-call_true-valid-memsafety_false-termination.c, a3e8e2f2e732e3d055a8530bee1dde0ce1d9b0781c95b8d367dc12736fc0ac3f
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/a3e8e2f2e732e3d055a8530bee1dde0ce1d9b0781c95b8d367dc12736fc0ac3f.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_14_false-unreach-call_true-valid-memsafety_false-termination.c, a3e8e2f2e732e3d055a8530bee1dde0ce1d9b0781c95b8d367dc12736fc0ac3f
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/a3e8e2f2e732e3d055a8530bee1dde0ce1d9b0781c95b8d367dc12736fc0ac3f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 21 witnesses for program sv-benchmarks/c/locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c, a3e8e2f2e732e3d055a8530bee1dde0ce1d9b0781c95b8d367dc12736fc0ac3f
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/a3e8e2f2e732e3d055a8530bee1dde0ce1d9b0781c95b8d367dc12736fc0ac3f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
af79623 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 25 | 2019-11-30T03:05:03+01:00 | ||
da10188 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 25 | 2019-12-01T15:39:01+01:00 | ||
1a5a047 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 4 | 2019-12-01 14:04:27 | ||
287ed89 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 15 | 2019-12-04T00:53 CET (comp) | ||
d5e3e87 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 27 | 2019-12-11T21:48:11+01:00 | 766196b | |
8f7aaa5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 24 | 2019-12-11T21:45:27+01:00 | 8c7ba8c | |
afa1cc8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 23 | 2019-12-11T21:09:05+01:00 | 1a5a047 | |
5a1c40d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 27 | 2019-12-11T20:44:26+01:00 | b09d9dd | |
3138c25 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 27 | 2019-12-08T01:51:32+01:00 | 130af7f | |
8fae652 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 24 | 2019-12-08T00:26:18+01:00 | 868e801 | |
16238f0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 25 | 2019-12-07T21:14:34+01:00 | 16d9d14 | |
2e395cf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 22 | 2019-12-05T20:20:12+01:00 | 0030ece | |
d769713 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 22 | 2019-12-04T02:58:19+01:00 | 287ed89 | |
8629dc6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 37 | 2019-12-03T08:09:07+01:00 | 2508fa9 | |
2508fa9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 33 | 2019-11-30T07:43:50+01:00 | ||
130af7f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8 | 27 | 2019-12-07T11:01:43+01:00 | ||
766196b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 27 | 2019-12-01T00:14:19+01:00 | ||
827d41d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 26 | 2019-12-11T20:54:21+01:00 | 4c6a59d | |
98f2963 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 26 | 2019-12-05T19:34:01+01:00 | 2db2398 | |
c94cda1 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.9 | 42 | 2019-11-30T05:21:58+01:00 | ||
86c4c5d | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 42 | 2019-11-30T22:31:17+01:00 |
Found 26 witnesses for program sv-benchmarks/c/locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c, a3e8e2f2e732e3d055a8530bee1dde0ce1d9b0781c95b8d367dc12736fc0ac3f
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/a3e8e2f2e732e3d055a8530bee1dde0ce1d9b0781c95b8d367dc12736fc0ac3f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
60e2f9d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T03:36 CET (sv-comp) | ||
247009f | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 25 | 2018-12-07T12:18:14+01:00 | ||
324cb4f | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 25 | 2018-12-05T14:41:34+01:00 | ||
a4f4dd1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 7 | 2018-12-08T20:50 CET (sv-comp) | ||
76c001e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 7 | 2018-12-07T23:09:06 | ||
e143e74 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 25 | 2018-12-10T17:24:45+01:00 | ||
b67ec0d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 22 | 2018-12-06T23:53:39+01:00 | ||
6d50b4c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-10T20:35:57+01:00 | e143e74 | |
44cfc67 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 25 | 2018-12-09T20:18:45+01:00 | 72cdd5f | |
46ab531 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-09T18:07:03+01:00 | e539d2d | |
f0fc90a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-08T23:42:23+01:00 | a4f4dd1 | |
48ccd83 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 24 | 2018-12-08T22:10:57+01:00 | 76c001e | |
3968d8e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 26 | 2018-12-08T08:33:06+01:00 | b67ec0d | |
b630bee | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 30 | 2018-12-08T05:04:48+01:00 | 393eb1b | |
d8342c1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-07T18:26:23+01:00 | 93d888c | |
df49d9b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 30 | 2018-12-06T10:18:51+01:00 | 31c1a4e | |
a7beb27 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 38 | 2018-12-06T09:47:55+01:00 | d33d5fc | |
6d05f64 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-06T09:19:33+01:00 | 9b08a18 | |
d33d5fc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 33 | 2018-12-05T18:25:57+01:00 | ||
8a5f499 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 25 | 2018-12-09T20:53:12+01:00 | 55a1774 | |
b175d72 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 25 | 2018-12-09T20:36:57+01:00 | 0529819 | |
df362f3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 26 | 2018-12-06T09:41:15+01:00 | 483a165 | |
65c9d6c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 26 | 2018-12-06T09:18:04+01:00 | 9b1f1bb | |
42686c6 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 42 | 2018-12-08T04:12:18+01:00 | ||
7d6a464 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 42 | 2018-12-09T20:39:27+01:00 | ||
aa6da55 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 42 | 2018-12-06T06:17:41+01:00 |
Found 26 witnesses for program sv-benchmarks/c/locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c, a3e8e2f2e732e3d055a8530bee1dde0ce1d9b0781c95b8d367dc12736fc0ac3f
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/a3e8e2f2e732e3d055a8530bee1dde0ce1d9b0781c95b8d367dc12736fc0ac3f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
8db4e85 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T23:36 CET (sv-comp) | ||
db580b1 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T10:49:59.473372 | ||
0579024 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 3.1 | 92 | 2017-12-01T09:40 CET (sv-comp) | ||
c076baf | 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 | 40 | 2017-12-03T06:53Z | ||
8ade640 | 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 | 41 | 2017-12-03T04:14Z | ||
04bcf13 | 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 | 40 | 2017-12-03T03:41Z | ||
c3ab2ba | 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 | 63 | 2017-12-01T08:23 CET (sv-comp) | ||
6e6b187 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | skink | 3 | 2017-12-01T22:28 CET (sv-comp) | ||
08667f2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 31 | 2017-12-02T21:50Z | ||
1489aa1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 2 | 2017-12-02T16:40 CET (sv-comp) | ||
4c3d5ec | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 30 | 2017-12-02T15:16Z | ||
1f381a0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 7 | 2017-12-01T12:54:05.837455 | ||
5049016 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 7 | 2017-12-01T08:38:51.470353 | ||
10f0d57 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 10 | 2017-12-01T18:28 CET (sv-comp) | ||
a5a5292 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 10 | 2017-12-01T02:38 CET (sv-comp) | ||
d50599c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn | 25 | 2017-12-02T22:12:49+01:00 | ||
c3619bc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 19 | 2017-12-01T03:44:43+01:00 | ||
bc9d90d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 49 | 2017-11-30T16:55:47+01:00 | ||
b907bc5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 12 | 2017-11-30T19:46:53+01:00 | ||
a314e60 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 12 | 2017-12-01T20:59:29+01:00 | ||
9904937 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 19 | 2017-11-30T21:23 CET (sv-comp) | ||
45dd5b2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 31 | 2017-12-02T17:10Z | ||
c02df58 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 24 | 2017-11-30T19:43 CET (sv-comp) | ||
0b4a993 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 42 | 2017-12-01T13:09:24+01:00 | ||
70483bd | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Automizer | 35 | 2017-12-03T11:13Z | ||
e515845 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 26 | 2017-12-01T14:25 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c, a3e8e2f2e732e3d055a8530bee1dde0ce1d9b0781c95b8d367dc12736fc0ac3f
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/a3e8e2f2e732e3d055a8530bee1dde0ce1d9b0781c95b8d367dc12736fc0ac3f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |