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/ldv-memsafety/StructInitialization2_true-valid-memsafety.c |
programSHA | a9e57556025294612a4983c83f08462039130a71f3900642f3b13b79e1ecf173 |
witnessName | results-verified/cbmc.2018-12-04_2248.logfiles/sv-comp19_prop-memsafety.StructInitialization2_true-valid-memsafety.c.files/witness.graphml |
witnessSHA | b4805f642eed4ae21d458bde1e60db7eeb754a1ed340000a0974b62cdd32a305 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-06T00:35 CET (sv-comp) |
error-specification-length | Key 'specification' longer than 100 characters. |
producer | CBMC |
programfile | ../../sv-benchmarks/c/ldv-memsafety/StructInitialization2_true-valid-memsafety.c |
programhash | 40aebfbfcf1ace3ae19699b445fb033c37125741 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) |
witness-file | witnessFileByHash/b4805f642eed4ae21d458bde1e60db7eeb754a1ed340000a0974b62cdd32a305.graphml |
witness-sha256 | b4805f642eed4ae21d458bde1e60db7eeb754a1ed340000a0974b62cdd32a305 |
witness-size | 3507 |
witness-type | correctness_witness |
Found 17 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization2_true-valid-memsafety.c, a9e57556025294612a4983c83f08462039130a71f3900642f3b13b79e1ecf173
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/a9e57556025294612a4983c83f08462039130a71f3900642f3b13b79e1ecf173.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c3264df | Inspect | valid-memsafety | correctness_witness | DIVINE 4 | 2 | 2023-12-18T10:02:11+01:00 | ||
1c943fd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T21:02:27Z | ||
acda2d6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-11-30T07:27:01+01:00 | ||
76d0fdf | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 3 | 2023-12-03T22:57:43+01:00 | ||
19a74a1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2023-12-18T17:53:57+01:00 | ||
b5436ac | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 3 | 2023-12-18T01:52:21+01:00 | ||
d62a3c4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-05T09:47:28Z | ||
dc92a6c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-04T14:50:08Z | ||
682b773 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-01T20:50:49Z | ||
e7b5baa | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 7.4.0 incr | 3 | 2023-12-01T14:01:12Z | ||
a957a1d | 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 | 121 | 2023-12-02T17:05:20Z | ||
8f0f12c | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | PredatorHP | 4 | 2023-11-30T08:26:14Z | ||
7c29f10 | 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 | 121 | 2023-12-02T23:55:11Z | ||
0032fd2 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 4 | 2023-12-01T01:34:55Z | ||
5d4bb71 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CBMC | 14 | 2023-12-17T19:30:58+01:00 | ||
da754ea | 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 | 121 | 2023-11-28T23:27:09Z | ||
97bc92c | 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 | 5 | 2023-11-30T22:47:28+01:00 |
Found 13 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization2_true-valid-memsafety.c, a9e57556025294612a4983c83f08462039130a71f3900642f3b13b79e1ecf173
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/a9e57556025294612a4983c83f08462039130a71f3900642f3b13b79e1ecf173.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9e4085c | Inspect | valid-memsafety | correctness_witness | DIVINE 4 | 2 | 2022-12-09T05:12:49+01:00 | ||
015ef12 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2022-12-10T18:22:09+01:00 | ||
3655630 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 3 | 2022-12-12T00:38:56+01:00 | ||
82f3f99 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2022-12-10T01:25:22+01:00 | ||
8293b0a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 3 | 2022-12-09T02:14:18+01:00 | ||
c992be2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2022-12-08T20:05:09Z | ||
7fa3fda | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 7.0.0 incr | 3 | 2022-12-19T00:41:05Z | ||
a45d23b | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 6.8.0 incr | 3 | 2022-12-25T10:33:53Z | ||
6ab71a1 | 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 | 121 | 2022-12-14T04:01:59Z | ||
170e334 | 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 | 121 | 2022-12-14T18:35:41Z | ||
b510f8d | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CBMC | 14 | 2022-12-08T11:52:48+01:00 | ||
362da58 | 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 | 121 | 2022-12-13T12:14:04Z | ||
bd53028 | 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 | 5 | 2022-12-08T01:00:34+01:00 |
Found 11 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization2_true-valid-memsafety.c, a9e57556025294612a4983c83f08462039130a71f3900642f3b13b79e1ecf173
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/a9e57556025294612a4983c83f08462039130a71f3900642f3b13b79e1ecf173.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
8ebdd66 | Inspect | valid-memsafety | correctness_witness | DIVINE 4 | 2 | 2021-12-07T09:17:49+01:00 | ||
dd0f58c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-05T15:37:46+01:00 | ||
268d0b0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 3 | 2021-12-08T18:09:33+01:00 | ||
7ef469a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2021-12-09T13:28:06+01:00 | ||
ab0a520 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 3 | 2021-12-07T03:36:38+01:00 | ||
df4ba61 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 6.8.0 incr | 3 | 2021-12-08T09:52:23Z | ||
a73bcc1 | 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 | 121 | 2021-12-10T00:21:27Z | ||
45b8ebf | 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 | 121 | 2021-12-10T08:58:40Z | ||
641eea0 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CBMC | 6 | 2021-12-06T10:19:38+01:00 | ||
6772a64 | 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 | 121 | 2021-12-06T21:48:26Z | ||
34813ac | 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 | 5 | 2021-12-06T00:00:08+01:00 |
Found 3 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization2_true-valid-memsafety.c, a9e57556025294612a4983c83f08462039130a71f3900642f3b13b79e1ecf173
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/a9e57556025294612a4983c83f08462039130a71f3900642f3b13b79e1ecf173.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
42fd0e4 | Inspect | valid-memsafety | correctness_witness | DIVINE 4 | 2 | 2020-12-06T18:38:57+01:00 | ||
e08d204 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 3 | 2020-12-05T13:27:25+01:00 | ||
51f1653 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2020-12-07T23:47:23+01:00 |
Found 2 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization2_true-valid-memsafety.c, a9e57556025294612a4983c83f08462039130a71f3900642f3b13b79e1ecf173
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/a9e57556025294612a4983c83f08462039130a71f3900642f3b13b79e1ecf173.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7ee6ee0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 3 | 2019-11-30T06:53:05+01:00 | ||
46c3680 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 3 | 2019-12-01T15:51:27+01:00 |
Found 3 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization2_true-valid-memsafety.c, a9e57556025294612a4983c83f08462039130a71f3900642f3b13b79e1ecf173
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/a9e57556025294612a4983c83f08462039130a71f3900642f3b13b79e1ecf173.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
65085c1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T06:58 CET (sv-comp) | ||
62cbeb5 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 3 | 2018-12-07T07:53:38+01:00 | ||
b9a7db3 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T02:44:17+01:00 |
Found 8 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization2_true-valid-memsafety.c, a9e57556025294612a4983c83f08462039130a71f3900642f3b13b79e1ecf173
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/a9e57556025294612a4983c83f08462039130a71f3900642f3b13b79e1ecf173.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
a3778f7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2017-12-03T00:30 CET (sv-comp) | ||
b9f3bb2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.6.1-svn | 5 | 2017-12-01T09:36:50+01:00 | ||
efd8ea9 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T11:12:55.023380 | ||
7d9e706 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T23:42:43.976375 | ||
6996f28 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 3 | 2017-12-01T08:23:58+01:00 | ||
b075ca0 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Map2Check | 2 | 2017-12-01T23:31 CET (sv-comp) | ||
c383d75 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CBMC | 4 | 2017-12-01T08:30 CET (sv-comp) | ||
3bd8f9d | 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 | 5 | 2017-12-01T08:19 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization2_true-valid-memsafety.c, a9e57556025294612a4983c83f08462039130a71f3900642f3b13b79e1ecf173
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/a9e57556025294612a4983c83f08462039130a71f3900642f3b13b79e1ecf173.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |