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/list-properties/list_true-unreach-call_false-valid-memtrack.i |
programSHA | 26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99 |
witnessName | results-verified/cpa-seq.2018-12-05_0546.logfiles/sv-comp19_prop-reachsafety.list_true-unreach-call_false-valid-memtrack.i.files/witness.graphml |
witnessSHA | 49bb96e037e5893fbf4fec239f7bbeb3903dd71de7d3e018cbdfa473df5b19fb |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-05T09:39:33+01:00 |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | 26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99 |
programfile | ../../sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i |
programhash | 26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/49bb96e037e5893fbf4fec239f7bbeb3903dd71de7d3e018cbdfa473df5b19fb.graphml |
witness-sha256 | 49bb96e037e5893fbf4fec239f7bbeb3903dd71de7d3e018cbdfa473df5b19fb |
witness-size | 10664 |
witness-type | correctness_witness |
This witness was created for this program (cf. table above, 26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99).
Found 0 witnesses for program sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i, 26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i, 26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i, 26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i, 26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i, 26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 20 witnesses for program sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i, 26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
d135ecc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T07:30 CET (sv-comp) | ||
1779cdd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-10T10:48:58+01:00 | 49c1cd2 | |
a79d5b0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T23:43:40+01:00 | d135ecc | |
bf91378 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 10 | 2018-12-07T21:44:35+01:00 | ||
d65d55e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-08T04:54:37+01:00 | 6d23772 | |
8233bb5 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-07T09:26:13+01:00 | 596c526 | |
cea9620 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-06T09:41:46+01:00 | e369631 | |
8a87936 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-05T23:42:49+01:00 | ||
c6fc243 | 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-08T02:57:38 | ||
d1adac8 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T03:52:32+01:00 | 49c1cd2 | |
597a3e1 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-07T01:13:34+01:00 | a839745 | |
d1891d7 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-08T22:10:05+01:00 | c6fc243 | |
602534d | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-06T10:19:35+01:00 | 10f70b0 | |
d62a729 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T12:35:18 | ||
2cf8670 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 11 | 2018-12-07T05:33:23+01:00 | ||
c41a228 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T21:43:54+01:00 | d62a729 | |
66b488b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-08T07:15:13+01:00 | 2cf8670 | |
5a1f3a7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-07T09:07:06+01:00 | a7bcba7 | |
d0a8c62 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-06T09:28:06+01:00 | 49bb96e | |
49bb96e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 11 | 2018-12-05T09:39:33+01:00 |
Found 0 witnesses for program sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i, 26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i, 26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |