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_15_false-unreach-call_true-valid-memsafety_false-termination.c |
programSHA | af580c85929f0ce2231633c74050b4f874b6060bba20de2c6fa78a3539add601 |
witnessName | results-verified/esbmc-kind.2018-12-06_1103.logfiles/sv-comp19_prop-memsafety.test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c.files/witness.graphml |
witnessSHA | a7a542e21ddd4ddeaa1ae8ff716c5e9f472f78d81178d412a40ff63144d4ff36 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-07T07:13:51.744951 |
producer | ESBMC 6.0.0 kind |
programfile | ../../sv-benchmarks/c/locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c |
programhash | 4892275a211cad54ffe3d940980c258aec58e47d |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
witness-file | witnessFileByHash/a7a542e21ddd4ddeaa1ae8ff716c5e9f472f78d81178d412a40ff63144d4ff36.graphml |
witness-sha256 | a7a542e21ddd4ddeaa1ae8ff716c5e9f472f78d81178d412a40ff63144d4ff36 |
witness-size | 3444 |
witness-type | correctness_witness |
Found 0 witnesses for program sv-benchmarks/c/locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c, af580c85929f0ce2231633c74050b4f874b6060bba20de2c6fa78a3539add601
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/af580c85929f0ce2231633c74050b4f874b6060bba20de2c6fa78a3539add601.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_false-unreach-call_true-valid-memsafety_false-termination.c, af580c85929f0ce2231633c74050b4f874b6060bba20de2c6fa78a3539add601
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/af580c85929f0ce2231633c74050b4f874b6060bba20de2c6fa78a3539add601.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_false-unreach-call_true-valid-memsafety_false-termination.c, af580c85929f0ce2231633c74050b4f874b6060bba20de2c6fa78a3539add601
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/af580c85929f0ce2231633c74050b4f874b6060bba20de2c6fa78a3539add601.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_false-unreach-call_true-valid-memsafety_false-termination.c, af580c85929f0ce2231633c74050b4f874b6060bba20de2c6fa78a3539add601
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/af580c85929f0ce2231633c74050b4f874b6060bba20de2c6fa78a3539add601.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_15_false-unreach-call_true-valid-memsafety_false-termination.c, af580c85929f0ce2231633c74050b4f874b6060bba20de2c6fa78a3539add601
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/af580c85929f0ce2231633c74050b4f874b6060bba20de2c6fa78a3539add601.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
88d0e67 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.9 | 27 | 2019-11-30T02:23:52+01:00 | ||
3e9bc7e | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 27 | 2019-12-01T03:27:40+01:00 | ||
f11ff64 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 4 | 2019-12-01 21:31:29 | ||
4e109ae | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 16 | 2019-12-04T00:35 CET (comp) | ||
fdd3359 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 26 | 2019-12-11T21:54:17+01:00 | 5c6767c | |
421e99d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 46 | 2019-12-11T21:52:56+01:00 | 22fe275 | |
30075a0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 24 | 2019-12-11T21:09:40+01:00 | f11ff64 | |
550e9c9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 28 | 2019-12-11T20:44:35+01:00 | 37c4699 | |
4094320 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 46 | 2019-12-08T01:51:17+01:00 | acfdeae | |
3b146b4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 26 | 2019-12-08T00:26:20+01:00 | d670099 | |
0c02054 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 27 | 2019-12-07T21:16:40+01:00 | 6ebd701 | |
00cab4b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 23 | 2019-12-05T20:20:52+01:00 | e2306af | |
adaa1c0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 23 | 2019-12-04T02:58:18+01:00 | 4e109ae | |
f5339d6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 39 | 2019-12-03T08:07:42+01:00 | f1d57ab | |
f1d57ab | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 34 | 2019-11-30T08:08:09+01:00 | ||
acfdeae | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8 | 46 | 2019-12-07T22:34:19+01:00 | ||
22fe275 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 46 | 2019-12-01T01:36:44+01:00 | ||
51a47f4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 27 | 2019-12-11T20:54:20+01:00 | d1adee7 | |
dcffa1f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 27 | 2019-12-05T19:34:17+01:00 | 660ccdf | |
17bb9d7 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.9 | 49 | 2019-11-30T04:02:04+01:00 | ||
b940d99 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 49 | 2019-12-01T01:50:51+01:00 |
Found 25 witnesses for program sv-benchmarks/c/locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c, af580c85929f0ce2231633c74050b4f874b6060bba20de2c6fa78a3539add601
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/af580c85929f0ce2231633c74050b4f874b6060bba20de2c6fa78a3539add601.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e6f6d91 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T05:47 CET (sv-comp) | ||
e5ee413 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 27 | 2018-12-08T02:03:56+01:00 | ||
c7fbce7 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-06T02:49:52+01:00 | ||
eba4c6c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 8 | 2018-12-08T09:40 CET (sv-comp) | ||
ad827c4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 7 | 2018-12-08T10:44:40 | ||
41a24c8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 42 | 2018-12-10T17:16:19+01:00 | ||
cd2cf99 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 22 | 2018-12-08T00:59:45+01:00 | ||
6887358 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 46 | 2018-12-10T20:37:36+01:00 | 41a24c8 | |
7cc9821 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 26 | 2018-12-09T20:17:11+01:00 | b853efc | |
ac41b51 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 28 | 2018-12-09T18:20:41+01:00 | 6c96e3a | |
92ebde4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 28 | 2018-12-08T23:42:10+01:00 | eba4c6c | |
9c38c25 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 40 | 2018-12-08T22:11:00+01:00 | ad827c4 | |
61a4b6e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-08T09:04:36+01:00 | cd2cf99 | |
f12ae74 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 32 | 2018-12-08T04:57:12+01:00 | 8fa2b3c | |
8933674 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 24 | 2018-12-07T18:47:18+01:00 | 8004505 | |
a196278 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 32 | 2018-12-06T10:20:10+01:00 | efcdf42 | |
fabb1d8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 39 | 2018-12-06T09:47:58+01:00 | 0fb2f22 | |
62ef79f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 24 | 2018-12-06T09:20:16+01:00 | 7cdc05c | |
0fb2f22 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 35 | 2018-12-05T15:58:24+01:00 | ||
406633e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-09T20:53:11+01:00 | 4ba55ce | |
8777062 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-09T20:35:25+01:00 | 537c722 | |
4ad972a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-06T09:41:35+01:00 | d995cdf | |
cb01d86 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 48 | 2018-12-08T02:11:22+01:00 | ||
932d96e | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 45 | 2018-12-09T20:36:56+01:00 | ||
5d5b268 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 49 | 2018-12-06T01:43:23+01:00 |
Found 26 witnesses for program sv-benchmarks/c/locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c, af580c85929f0ce2231633c74050b4f874b6060bba20de2c6fa78a3539add601
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/af580c85929f0ce2231633c74050b4f874b6060bba20de2c6fa78a3539add601.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
a1906bf | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T23:40 CET (sv-comp) | ||
de0be94 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T11:50:53.011201 | ||
6c0a1ac | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 3.1 | 101 | 2017-12-01T09:46 CET (sv-comp) | ||
3454f0d | 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:54Z | ||
37e94f3 | 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-03T04:24Z | ||
fe7de68 | 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:08Z | ||
b64c6ea | 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 | 67 | 2017-12-01T08:24 CET (sv-comp) | ||
830f177 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | skink | 3 | 2017-12-01T23:20 CET (sv-comp) | ||
5d68c23 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 33 | 2017-12-02T20:16Z | ||
8fb3d43 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 2 | 2017-12-02T14:54 CET (sv-comp) | ||
002ad6c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 31 | 2017-12-02T18:12Z | ||
b24a92b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 7 | 2017-12-01T23:29:45.744488 | ||
7a0ce51 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 7 | 2017-12-01T11:05:20.237855 | ||
5d1a956 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 10 | 2017-12-01T21:10 CET (sv-comp) | ||
abd2c41 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 10 | 2017-11-30T17:56 CET (sv-comp) | ||
e77d77b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn | 42 | 2017-12-02T20:23:47+01:00 | ||
f9d1363 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 32 | 2017-11-30T15:30:47+01:00 | ||
fdc0aec | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 48 | 2017-11-30T16:01:03+01:00 | ||
394d6c0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 13 | 2017-11-30T18:11:14+01:00 | ||
9748df8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 13 | 2017-12-01T22:26:06+01:00 | ||
69e7a0e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 20 | 2017-12-01T01:36 CET (sv-comp) | ||
bb1b8e9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 33 | 2017-12-02T14:44Z | ||
69040f1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 25 | 2017-11-30T22:20 CET (sv-comp) | ||
928e0ed | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 48 | 2017-12-01T14:20:38+01:00 | ||
bb2c674 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Automizer | 37 | 2017-12-03T11:14Z | ||
028dfe3 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 27 | 2017-12-01T14:13 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c, af580c85929f0ce2231633c74050b4f874b6060bba20de2c6fa78a3539add601
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/af580c85929f0ce2231633c74050b4f874b6060bba20de2c6fa78a3539add601.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |