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_12_true-unreach-call_true-valid-memsafety_false-termination.c |
programSHA | fa371f3bd2fca0acf910c7e8424a3d7f8ec147b8d9d0106fd2977c696d02d737 |
witnessName | results-verified/pesco.2018-12-06_1244.logfiles/sv-comp19_prop-reachsafety.test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c.files/witness.graphml |
witnessSHA | 14b971451080c432180fc3f1eb55bef7262d04b2cbfc4240fb505effb5369ded |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-07T19:07:42+01:00 |
producer | CPAchecker 1.7-svn b8d6131600+ |
program-sha256 | fa371f3bd2fca0acf910c7e8424a3d7f8ec147b8d9d0106fd2977c696d02d737 |
programfile | ../../sv-benchmarks/c/locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c |
programhash | fa371f3bd2fca0acf910c7e8424a3d7f8ec147b8d9d0106fd2977c696d02d737 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/14b971451080c432180fc3f1eb55bef7262d04b2cbfc4240fb505effb5369ded.graphml |
witness-sha256 | 14b971451080c432180fc3f1eb55bef7262d04b2cbfc4240fb505effb5369ded |
witness-size | 22402 |
witness-type | correctness_witness |
This witness was created for this program (cf. table above, fa371f3bd2fca0acf910c7e8424a3d7f8ec147b8d9d0106fd2977c696d02d737).
Found 0 witnesses for program sv-benchmarks/c/locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c, fa371f3bd2fca0acf910c7e8424a3d7f8ec147b8d9d0106fd2977c696d02d737
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/fa371f3bd2fca0acf910c7e8424a3d7f8ec147b8d9d0106fd2977c696d02d737.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_12_true-unreach-call_true-valid-memsafety_false-termination.c, fa371f3bd2fca0acf910c7e8424a3d7f8ec147b8d9d0106fd2977c696d02d737
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/fa371f3bd2fca0acf910c7e8424a3d7f8ec147b8d9d0106fd2977c696d02d737.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_12_true-unreach-call_true-valid-memsafety_false-termination.c, fa371f3bd2fca0acf910c7e8424a3d7f8ec147b8d9d0106fd2977c696d02d737
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/fa371f3bd2fca0acf910c7e8424a3d7f8ec147b8d9d0106fd2977c696d02d737.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_12_true-unreach-call_true-valid-memsafety_false-termination.c, fa371f3bd2fca0acf910c7e8424a3d7f8ec147b8d9d0106fd2977c696d02d737
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/fa371f3bd2fca0acf910c7e8424a3d7f8ec147b8d9d0106fd2977c696d02d737.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_12_true-unreach-call_true-valid-memsafety_false-termination.c, fa371f3bd2fca0acf910c7e8424a3d7f8ec147b8d9d0106fd2977c696d02d737
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/fa371f3bd2fca0acf910c7e8424a3d7f8ec147b8d9d0106fd2977c696d02d737.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
faa143a | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 22 | 2019-12-01T14:08:19+01:00 | ||
00c0473 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.9 | 22 | 2019-11-30T05:43:57+01:00 | ||
b09997d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 22 | 2019-12-11T20:23:51+01:00 | d249980 | |
6017a09 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 22 | 2019-12-11T20:14:49+01:00 | 629cd33 | |
511a9b7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 22 | 2019-12-11T20:02:18+01:00 | e9b10b6 | |
bdd608b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 22 | 2019-12-08T00:59:25+01:00 | 943ca40 | |
5fc8cf0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 22 | 2019-12-07T23:38:33+01:00 | 36ba470 | |
ae08d5f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 22 | 2019-12-07T19:41:38+01:00 | f7a8afd | |
f840a73 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 22 | 2019-12-05T19:02:51+01:00 | 64b84df | |
7c9f30e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 22 | 2019-11-30T17:23:43+01:00 | 55e9a6a | |
55e9a6a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 22 | 2019-11-30T09:41:14+01:00 | ||
943ca40 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8 | 22 | 2019-12-07T14:11:14+01:00 | ||
629cd33 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 22 | 2019-12-01T02:20:59+01:00 | ||
89a5d2e | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.9 | 40 | 2019-11-29T20:18:44+01:00 | ||
4420491 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 40 | 2019-12-01T00:13:42+01:00 |
Found 21 witnesses for program sv-benchmarks/c/locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c, fa371f3bd2fca0acf910c7e8424a3d7f8ec147b8d9d0106fd2977c696d02d737
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/fa371f3bd2fca0acf910c7e8424a3d7f8ec147b8d9d0106fd2977c696d02d737.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
1c8c928 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T06:29 CET (sv-comp) | ||
9f3b689 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-05T23:17:52+01:00 | ||
8888fb5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T02:20 CET (sv-comp) | ||
2bee1f0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T09:25:11 | ||
14b9714 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 22 | 2018-12-07T19:07:42+01:00 | ||
d11ab8a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-10T20:15:05+01:00 | 31925a1 | |
de77e59 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-09T20:28:16+01:00 | 5894d24 | |
46125a2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-09T20:10:00+01:00 | d0d26e8 | |
5ced93d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-09T19:59:46+01:00 | 8e5c281 | |
b309c8f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-08T23:10:33+01:00 | 8888fb5 | |
a6982fe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-08T21:29:09+01:00 | 2bee1f0 | |
5614ac1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-08T05:16:05+01:00 | 14b9714 | |
7273a51 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-08T04:27:37+01:00 | 5f193fa | |
58bb38f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-07T17:45:53+01:00 | 72110aa | |
9505dae | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-06T09:29:00+01:00 | 43c57b6 | |
bf60a7a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-06T08:45:50+01:00 | 104827b | |
8d23a76 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-06T08:13:32+01:00 | a0e8f2f | |
104827b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-05T23:51:35+01:00 | ||
2a278c8 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 40 | 2018-12-07T09:16:39+01:00 | ||
0f246d6 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 36 | 2018-12-09T20:40:50+01:00 | ||
d76f978 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 40 | 2018-12-06T07:14:46+01:00 |
Found 37 witnesses for program sv-benchmarks/c/locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c, fa371f3bd2fca0acf910c7e8424a3d7f8ec147b8d9d0106fd2977c696d02d737
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/fa371f3bd2fca0acf910c7e8424a3d7f8ec147b8d9d0106fd2977c696d02d737.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
f6cdb94 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T23:38 CET (sv-comp) | ||
ecf4a09 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T11:45:58.370741 | ||
97f068b | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 3.1 | 68 | 2017-12-01T09:55 CET (sv-comp) | ||
fcd71a6 | 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 | 34 | 2017-12-03T06:54Z | ||
9109a7c | 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 | 36 | 2017-12-03T03:55Z | ||
1aaf6b8 | 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 | 35 | 2017-12-03T03:39Z | ||
4d355f8 | 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 | 54 | 2017-12-01T08:19 CET (sv-comp) | ||
72110aa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | skink | 3 | 2017-12-01T22:11 CET (sv-comp) | ||
2278035 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Taipan | 35 | 2017-12-02T17:54Z | ||
10783dd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T05:14 CET (sv-comp) | ||
84d0ded | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Kojak | 36 | 2017-12-02T16:12Z | ||
232acc2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T04:41:33.500543 | ||
a0b78d8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 68 | 2017-12-01T19:39 CET (sv-comp) | ||
a79333f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 23 | 2017-12-03T02:08:04+01:00 | ||
e899c71 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-11-30T21:47:33+01:00 | ||
9028e34 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 22 | 2017-12-03T07:01:23+01:00 | 0a3b2ab | |
ac987f6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 23 | 2017-12-03T04:15:35+01:00 | f43e12e | |
81a0f22 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 22 | 2017-12-03T01:16:49+01:00 | c309166 | |
281ff3d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 22 | 2017-12-02T23:38:29+01:00 | 73a8131 | |
5c6567e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 22 | 2017-12-02T20:13:22+01:00 | 0dce00e | |
29f5afc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 22 | 2017-12-02T14:43:37+01:00 | ddf9019 | |
0d682dd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 22 | 2017-12-02T07:38:59+01:00 | 9be51b8 | |
61e19b8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 22 | 2017-12-02T00:06:25+01:00 | 7c18f38 | |
f365dc0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 22 | 2017-12-01T08:13:57+01:00 | e3936b1 | |
95f0094 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 22 | 2017-12-01T06:23:01+01:00 | f1b6024 | |
c6c08e1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 22 | 2017-12-01T05:25:53+01:00 | 7ed686f | |
6a0c674 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 22 | 2017-12-01T04:59:06+01:00 | df99339 | |
3c9fee5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 22 | 2017-12-01T04:22:06+01:00 | f85f846 | |
dcf9a5d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 22 | 2017-12-01T02:53:03+01:00 | ||
4a1e8c6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 24 | 2017-11-30T13:37:50+01:00 | ||
7f0f7cd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26725 | 22 | 2017-12-01T03:38:02+01:00 | ||
1551eb5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker (unknown version) | 21 | 2017-12-02T12:31:05+01:00 | ||
a8b13ec | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 35 | 2017-12-02T17:52Z | ||
bd735af | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 54 | 2017-11-30T20:30 CET (sv-comp) | ||
49fc171 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 40 | 2017-12-01T18:01:14+01:00 | ||
78ee22c | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Automizer | 28 | 2017-12-03T11:14Z | ||
496db17 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 23 | 2017-12-01T12:46 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c, fa371f3bd2fca0acf910c7e8424a3d7f8ec147b8d9d0106fd2977c696d02d737
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/fa371f3bd2fca0acf910c7e8424a3d7f8ec147b8d9d0106fd2977c696d02d737.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |