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).
Found 0 witnesses for program sv-benchmarks/c/memsafety/test-0232_false-valid-memtrack.i, f815fca5cb4e3d28ab5a5191e1f8f4aa5035e46e1405135a8e6b714ded762c2f
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/f815fca5cb4e3d28ab5a5191e1f8f4aa5035e46e1405135a8e6b714ded762c2f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/memsafety/test-0232_false-valid-memtrack.i, f815fca5cb4e3d28ab5a5191e1f8f4aa5035e46e1405135a8e6b714ded762c2f
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/f815fca5cb4e3d28ab5a5191e1f8f4aa5035e46e1405135a8e6b714ded762c2f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/memsafety/test-0232_false-valid-memtrack.i, f815fca5cb4e3d28ab5a5191e1f8f4aa5035e46e1405135a8e6b714ded762c2f
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/f815fca5cb4e3d28ab5a5191e1f8f4aa5035e46e1405135a8e6b714ded762c2f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/memsafety/test-0232_false-valid-memtrack.i, f815fca5cb4e3d28ab5a5191e1f8f4aa5035e46e1405135a8e6b714ded762c2f
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/f815fca5cb4e3d28ab5a5191e1f8f4aa5035e46e1405135a8e6b714ded762c2f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/memsafety/test-0232_false-valid-memtrack.i, f815fca5cb4e3d28ab5a5191e1f8f4aa5035e46e1405135a8e6b714ded762c2f
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/f815fca5cb4e3d28ab5a5191e1f8f4aa5035e46e1405135a8e6b714ded762c2f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 14 witnesses for program sv-benchmarks/c/memsafety/test-0232_false-valid-memtrack.i, f815fca5cb4e3d28ab5a5191e1f8f4aa5035e46e1405135a8e6b714ded762c2f
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/f815fca5cb4e3d28ab5a5191e1f8f4aa5035e46e1405135a8e6b714ded762c2f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
dc2d1d4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T16:03 CET (sv-comp) | ||
58215c2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-10T10:48:51+01:00 | 4433a0d | |
6266005 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T23:43:48+01:00 | dc2d1d4 | |
1a6741a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 6 | 2018-12-07T14:40:27+01:00 | ||
0a8806f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-05T19:50:33+01:00 | ||
0dace11 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-07T09:26:02+01:00 | 0c61788 | |
090bb8e | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T09:42:41+01:00 | 7e04008 | |
cee8cae | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T22:09:54+01:00 | 8c583e6 | |
622bd1c | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T10:20:24+01:00 | 46d464a | |
8c583e6 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | SMACK 1.9.3 | 3 | 2018-12-08T16:03:36 | ||
9088983 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T04:33:30+01:00 | 4433a0d | |
31f52e9 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-07T01:04:47+01:00 | cb0a4b0 | |
90523e1 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T05:05:30+01:00 | 3b7f2f8 | |
a65253f | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T09:19:30+01:00 | 9413408 |
Found 8 witnesses for program sv-benchmarks/c/memsafety/test-0232_false-valid-memtrack.i, f815fca5cb4e3d28ab5a5191e1f8f4aa5035e46e1405135a8e6b714ded762c2f
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/f815fca5cb4e3d28ab5a5191e1f8f4aa5035e46e1405135a8e6b714ded762c2f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
1204bea | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2017-12-02T23:47 CET (sv-comp) | ||
0c61788 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | PredatorHP | 4 | 2017-12-01T22:04 CET (sv-comp) | ||
829fe73 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Map2Check | 2 | 2017-12-01T23:36 CET (sv-comp) | ||
e42b951 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T11:46:35.840453 | ||
eebc47f | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T23:33:44.118355 | ||
b641bf1 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 3.1 | 4 | 2017-12-01T09:24 CET (sv-comp) | ||
1da4aa9 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CBMC | 11 | 2017-12-01T08:24 CET (sv-comp) | ||
44730fa | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | 2LS | 5 | 2017-12-01T08:19 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/memsafety/test-0232_false-valid-memtrack.i, f815fca5cb4e3d28ab5a5191e1f8f4aa5035e46e1405135a8e6b714ded762c2f
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/f815fca5cb4e3d28ab5a5191e1f8f4aa5035e46e1405135a8e6b714ded762c2f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |