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/heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i |
programSHA | 53f0c21e14ab2a1470bad0ad74eddfdc599517d52dfdca07e221d15b8722d095 |
witnessName | results-validated/cpa-seq-validate-violation-witnesses-divine-smt.2018-12-08_0324.logfiles/sv-comp19_prop-memsafety.dancing_true-unreach-call_false-valid-memtrack.i.files/witness.graphml |
witnessSHA | 55a1251236a6adfb319ed62ee2dfc68a08602356ab1d591915d026622eea44c1 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-08T03:54:58+01:00 |
inputwitnesshash | 52548e77a16e176b9298905c5cb50e9f23e2567558e0be89a18d1e45d99d2370 |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | 53f0c21e14ab2a1470bad0ad74eddfdc599517d52dfdca07e221d15b8722d095 |
programfile | ../../sv-benchmarks/c/heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i |
programhash | 53f0c21e14ab2a1470bad0ad74eddfdc599517d52dfdca07e221d15b8722d095 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G valid-deref) ) |
witness-file | witnessFileByHash/55a1251236a6adfb319ed62ee2dfc68a08602356ab1d591915d026622eea44c1.graphml |
witness-sha256 | 55a1251236a6adfb319ed62ee2dfc68a08602356ab1d591915d026622eea44c1 |
witness-size | 14415 |
witness-type | correctness_witness |
This witness was created for this program (cf. table above, 53f0c21e14ab2a1470bad0ad74eddfdc599517d52dfdca07e221d15b8722d095).
Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i, 53f0c21e14ab2a1470bad0ad74eddfdc599517d52dfdca07e221d15b8722d095
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/53f0c21e14ab2a1470bad0ad74eddfdc599517d52dfdca07e221d15b8722d095.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i, 53f0c21e14ab2a1470bad0ad74eddfdc599517d52dfdca07e221d15b8722d095
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/53f0c21e14ab2a1470bad0ad74eddfdc599517d52dfdca07e221d15b8722d095.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i, 53f0c21e14ab2a1470bad0ad74eddfdc599517d52dfdca07e221d15b8722d095
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/53f0c21e14ab2a1470bad0ad74eddfdc599517d52dfdca07e221d15b8722d095.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i, 53f0c21e14ab2a1470bad0ad74eddfdc599517d52dfdca07e221d15b8722d095
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/53f0c21e14ab2a1470bad0ad74eddfdc599517d52dfdca07e221d15b8722d095.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 11 witnesses for program sv-benchmarks/c/heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i, 53f0c21e14ab2a1470bad0ad74eddfdc599517d52dfdca07e221d15b8722d095
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/53f0c21e14ab2a1470bad0ad74eddfdc599517d52dfdca07e221d15b8722d095.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7a133df | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2019-12-01 21:48:28 | ||
f98e373 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 14 | 2019-12-11T21:42:36+01:00 | 29d520d | |
29d520d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 14 | 2019-11-30T21:26:49+01:00 | ||
88c5743 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 8 | 2019-12-08T00:06:06+01:00 | 6d566b2 | |
0dd8015 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.9 | 14 | 2019-12-11T20:54:54+01:00 | 5ef34e4 | |
132803b | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.9 | 14 | 2019-12-05T20:20:22+01:00 | 21f9a4b | |
e9c6728 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.9 | 14 | 2019-12-03T08:09:17+01:00 | 17f0c85 | |
17f0c85 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.9 | 14 | 2019-11-30T06:19:41+01:00 | ||
891ec61 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 15 | 2019-12-11T21:09:43+01:00 | 7a133df | |
6746bf5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 15 | 2019-11-30T09:18:44+01:00 | ||
70d5e7a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 15 | 2019-11-30T21:10:12+01:00 |
Found 12 witnesses for program sv-benchmarks/c/heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i, 53f0c21e14ab2a1470bad0ad74eddfdc599517d52dfdca07e221d15b8722d095
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/53f0c21e14ab2a1470bad0ad74eddfdc599517d52dfdca07e221d15b8722d095.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
bf95a53 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T11:38 CET (sv-comp) | ||
732f8d6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 14 | 2018-12-07T07:55:11+01:00 | ||
0ab2f6f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-08T23:44:30+01:00 | bf95a53 | |
c2ca711 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-08T22:11:14+01:00 | 311dc25 | |
f0f1fc6 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-07T09:19:58+01:00 | 3256cbf | |
c4f8094 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-08T05:06:13+01:00 | a1a1510 | |
bd7e206 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-06T09:17:33+01:00 | b512f92 | |
311dc25 | 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-08T01:28:13 | ||
55a1251 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-08T03:54:58+01:00 | 52548e7 | |
e8ac8a5 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-07T01:08:38+01:00 | 7510c0e | |
e1fcc48 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-06T10:18:13+01:00 | a8e9434 | |
5710e19 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T02:26:50 |
Found 11 witnesses for program sv-benchmarks/c/heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i, 53f0c21e14ab2a1470bad0ad74eddfdc599517d52dfdca07e221d15b8722d095
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/53f0c21e14ab2a1470bad0ad74eddfdc599517d52dfdca07e221d15b8722d095.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
33276c2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2017-12-02T23:37 CET (sv-comp) | ||
3256cbf | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | PredatorHP | 4 | 2017-12-01T22:08 CET (sv-comp) | ||
3c65b9e | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 kind | 5 | 2017-12-02T11:31:45.654238 | ||
50dbc07 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 incr | 6 | 2017-12-01T23:42:06.593070 | ||
7ddd3a5 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 3.1 | 5 | 2017-12-01T09:36 CET (sv-comp) | ||
c302f28 | 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 | 28 | 2017-12-01T08:21 CET (sv-comp) | ||
9f643ee | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Forester | 25 | 2017-12-01T19:38 CET (sv-comp) | ||
3b29ff9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 33 | 2017-12-02T13:38:48+01:00 | ||
bb39c16 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | PredatorHP | 4 | 2017-12-01T20:26 CET (sv-comp) | ||
0e03bc0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Forester | 25 | 2017-12-01T18:18 CET (sv-comp) | ||
f190d44 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 32 | 2017-11-30T21:24:31+01:00 |
Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i, 53f0c21e14ab2a1470bad0ad74eddfdc599517d52dfdca07e221d15b8722d095
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/53f0c21e14ab2a1470bad0ad74eddfdc599517d52dfdca07e221d15b8722d095.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |