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_true-unreach-call_true-valid-memsafety_false-termination.c |
programSHA | 147ca1da8af14892b786d395a06fd8b6200a60d045a94bb566b8a5fc764e5d16 |
witnessName | results-validated/cpa-seq-validate-violation-witnesses-uautomizer.2018-12-09_2030.logfiles/sv-comp19_prop-termination.test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c.files/witness.graphml |
witnessSHA | f76c175d1d14ab15aab2a40982d166f554b5a0f8047f481acef88c5156bca9f9 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-09T20:38:26+01:00 |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | 147ca1da8af14892b786d395a06fd8b6200a60d045a94bb566b8a5fc764e5d16 |
programfile | ../../sv-benchmarks/c/locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c |
programhash | 147ca1da8af14892b786d395a06fd8b6200a60d045a94bb566b8a5fc764e5d16 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(F end) ) |
witness-file | witnessFileByHash/f76c175d1d14ab15aab2a40982d166f554b5a0f8047f481acef88c5156bca9f9.graphml |
witness-sha256 | f76c175d1d14ab15aab2a40982d166f554b5a0f8047f481acef88c5156bca9f9 |
witness-size | 41052 |
witness-type | violation_witness |
This witness was created for this program (cf. table above, 147ca1da8af14892b786d395a06fd8b6200a60d045a94bb566b8a5fc764e5d16).
Found 0 witnesses for program sv-benchmarks/c/locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c, 147ca1da8af14892b786d395a06fd8b6200a60d045a94bb566b8a5fc764e5d16
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/147ca1da8af14892b786d395a06fd8b6200a60d045a94bb566b8a5fc764e5d16.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_true-unreach-call_true-valid-memsafety_false-termination.c, 147ca1da8af14892b786d395a06fd8b6200a60d045a94bb566b8a5fc764e5d16
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/147ca1da8af14892b786d395a06fd8b6200a60d045a94bb566b8a5fc764e5d16.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_true-unreach-call_true-valid-memsafety_false-termination.c, 147ca1da8af14892b786d395a06fd8b6200a60d045a94bb566b8a5fc764e5d16
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/147ca1da8af14892b786d395a06fd8b6200a60d045a94bb566b8a5fc764e5d16.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_true-unreach-call_true-valid-memsafety_false-termination.c, 147ca1da8af14892b786d395a06fd8b6200a60d045a94bb566b8a5fc764e5d16
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/147ca1da8af14892b786d395a06fd8b6200a60d045a94bb566b8a5fc764e5d16.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_14_true-unreach-call_true-valid-memsafety_false-termination.c, 147ca1da8af14892b786d395a06fd8b6200a60d045a94bb566b8a5fc764e5d16
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/147ca1da8af14892b786d395a06fd8b6200a60d045a94bb566b8a5fc764e5d16.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
8f69c26 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 25 | 2019-12-01T17:43:22+01:00 | ||
13c46ce | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.9 | 25 | 2019-11-30T12:36:19+01:00 | ||
ec1efdc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 25 | 2019-12-11T20:26:32+01:00 | 7f66e78 | |
238f0cb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 25 | 2019-12-11T20:18:55+01:00 | 332b3ec | |
153a05b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 25 | 2019-12-11T20:02:26+01:00 | 0f121e8 | |
c1690f0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 25 | 2019-12-08T00:36:53+01:00 | 2cae75c | |
de6d24e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 25 | 2019-12-07T23:40:13+01:00 | be404b6 | |
efa7a5b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 25 | 2019-12-07T19:46:49+01:00 | 3197981 | |
27a8002 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 25 | 2019-12-05T19:03:03+01:00 | 548bb39 | |
9386b6b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 25 | 2019-11-30T17:14:05+01:00 | acd26ff | |
acd26ff | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 25 | 2019-11-30T07:46:44+01:00 | ||
2cae75c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8 | 25 | 2019-12-07T21:54:35+01:00 | ||
332b3ec | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 25 | 2019-11-30T23:36:43+01:00 | ||
3b18967 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.9 | 47 | 2019-11-30T03:48:09+01:00 | ||
e865073 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 47 | 2019-12-01T01:33:46+01:00 |
Found 23 witnesses for program sv-benchmarks/c/locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c, 147ca1da8af14892b786d395a06fd8b6200a60d045a94bb566b8a5fc764e5d16
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/147ca1da8af14892b786d395a06fd8b6200a60d045a94bb566b8a5fc764e5d16.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
dd4f604 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T08:42 CET (sv-comp) | ||
f621624 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 25 | 2018-12-05T23:16:53+01:00 | ||
9485d2a | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 25 | 2018-12-08T03:20:19+01:00 | ||
fed41ed | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T12:13 CET (sv-comp) | ||
1d343a3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T08:43:19 | ||
75c3e6d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7 | 25 | 2018-12-10T18:10:38+01:00 | ||
1bf4576 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 25 | 2018-12-07T09:56:27+01:00 | ||
f2466ba | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 25 | 2018-12-10T19:39:49+01:00 | 75c3e6d | |
70ddacc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 25 | 2018-12-09T20:26:29+01:00 | 0b0e949 | |
cee4d70 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 25 | 2018-12-09T20:05:28+01:00 | 0926886 | |
780f1ac | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 25 | 2018-12-09T19:56:27+01:00 | ea5346a | |
e5fd26f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 25 | 2018-12-08T23:23:46+01:00 | fed41ed | |
461568e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 25 | 2018-12-08T21:27:58+01:00 | 1d343a3 | |
9bac780 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 25 | 2018-12-08T05:40:43+01:00 | 1bf4576 | |
2cbfac1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 25 | 2018-12-08T04:18:28+01:00 | 906ca8c | |
f488f4a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 25 | 2018-12-07T17:43:29+01:00 | 4d945ee | |
edc6bc8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 25 | 2018-12-06T09:28:19+01:00 | e73f6c5 | |
cb16519 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 25 | 2018-12-06T08:45:38+01:00 | 38ca48a | |
4eaa26e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 25 | 2018-12-06T07:18:44+01:00 | 72dff94 | |
38ca48a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 25 | 2018-12-06T02:33:20+01:00 | ||
6a02f7d | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 46 | 2018-12-06T21:19:02+01:00 | ||
f76c175 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 41 | 2018-12-09T20:38:26+01:00 | ||
8bb2bd9 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 47 | 2018-12-06T02:54:57+01:00 |
Found 35 witnesses for program sv-benchmarks/c/locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c, 147ca1da8af14892b786d395a06fd8b6200a60d045a94bb566b8a5fc764e5d16
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/147ca1da8af14892b786d395a06fd8b6200a60d045a94bb566b8a5fc764e5d16.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
041c4c7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T23:18 CET (sv-comp) | ||
fdfac8a | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T11:08:41.871360 | ||
83cd98a | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 3.1 | 85 | 2017-12-01T09:54 CET (sv-comp) | ||
8cf6899 | 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 | ||
20c70da | 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 | ||
89d752a | 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-03T04:20Z | ||
29ec6c0 | 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 | 62 | 2017-12-01T08:21 CET (sv-comp) | ||
4d945ee | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | skink | 3 | 2017-12-01T22:15 CET (sv-comp) | ||
9a0aac7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Taipan | 40 | 2017-12-02T23:26Z | ||
01aef2d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T06:20 CET (sv-comp) | ||
75cc0fb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Kojak | 42 | 2017-12-02T17:42Z | ||
dbe62f2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-01T17:53:37.123454 | ||
8491c21 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 85 | 2017-12-01T19:43 CET (sv-comp) | ||
fc2ed33 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 26 | 2017-12-02T22:52:39+01:00 | ||
91645a7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-12-01T05:46:10+01:00 | ||
b798636 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 25 | 2017-12-03T06:55:21+01:00 | d697c9d | |
94d6336 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 26 | 2017-12-03T04:30:30+01:00 | 699e37a | |
6557112 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 25 | 2017-12-03T02:57:07+01:00 | f4e19d4 | |
4d3040d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 25 | 2017-12-03T00:09:22+01:00 | d0a2b0d | |
22d4114 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 25 | 2017-12-02T20:55:00+01:00 | 93c7591 | |
5ac5f92 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 25 | 2017-12-02T07:36:30+01:00 | 511c33d | |
dcfb4e8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 25 | 2017-12-02T00:20:06+01:00 | df936da | |
a7fdf35 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 25 | 2017-12-01T08:14:01+01:00 | fe5cc32 | |
edf12db | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 25 | 2017-12-01T06:49:03+01:00 | 39467ef | |
e327e60 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 25 | 2017-12-01T06:20:29+01:00 | 47f33f5 | |
7a95c4c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 25 | 2017-12-01T06:15:41+01:00 | 771936e | |
67f0bc4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 25 | 2017-12-01T04:52:21+01:00 | 2d3703e | |
fac4975 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 25 | 2017-11-30T22:46:15+01:00 | ||
e4bcf7c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 27 | 2017-11-30T23:10:07+01:00 | ||
9263076 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26725 | 25 | 2017-11-30T16:53:40+01:00 | ||
c1ca504 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 40 | 2017-12-02T21:45Z | ||
2b56a22 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 62 | 2017-11-30T15:42 CET (sv-comp) | ||
28fa56a | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 46 | 2017-12-01T15:06:00+01:00 | ||
27f782a | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Automizer | 32 | 2017-12-03T11:12Z | ||
e97ec24 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 26 | 2017-12-01T13:14 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c, 147ca1da8af14892b786d395a06fd8b6200a60d045a94bb566b8a5fc764e5d16
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/147ca1da8af14892b786d395a06fd8b6200a60d045a94bb566b8a5fc764e5d16.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |