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/forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i |
programSHA | 29eb00db9ddbf891573926a49a39d5406ef24e5b25f4798a9c55519294619479 |
witnessName | results-validated/cpa-seq-validate-violation-witnesses-divine-smt.2018-12-08_0324.logfiles/sv-comp19_prop-memsafety.dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i.files/witness.graphml |
witnessSHA | 7d5b79391bd168131b63f1b2d72c121d07121bc341fdebc35ca70c25c0472fa5 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-08T04:07:33+01:00 |
inputwitnesshash | 946033308d7e855289e75755b474f194f38b0aff4aa8aecd710838a68d34b513 |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | 29eb00db9ddbf891573926a49a39d5406ef24e5b25f4798a9c55519294619479 |
programfile | ../../sv-benchmarks/c/forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i |
programhash | 29eb00db9ddbf891573926a49a39d5406ef24e5b25f4798a9c55519294619479 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G valid-memtrack) ) |
witness-file | witnessFileByHash/7d5b79391bd168131b63f1b2d72c121d07121bc341fdebc35ca70c25c0472fa5.graphml |
witness-sha256 | 7d5b79391bd168131b63f1b2d72c121d07121bc341fdebc35ca70c25c0472fa5 |
witness-size | 9872 |
witness-type | violation_witness |
This witness was created for this program (cf. table above, 29eb00db9ddbf891573926a49a39d5406ef24e5b25f4798a9c55519294619479).
Found 0 witnesses for program sv-benchmarks/c/forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i, 29eb00db9ddbf891573926a49a39d5406ef24e5b25f4798a9c55519294619479
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/29eb00db9ddbf891573926a49a39d5406ef24e5b25f4798a9c55519294619479.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i, 29eb00db9ddbf891573926a49a39d5406ef24e5b25f4798a9c55519294619479
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/29eb00db9ddbf891573926a49a39d5406ef24e5b25f4798a9c55519294619479.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i, 29eb00db9ddbf891573926a49a39d5406ef24e5b25f4798a9c55519294619479
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/29eb00db9ddbf891573926a49a39d5406ef24e5b25f4798a9c55519294619479.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i, 29eb00db9ddbf891573926a49a39d5406ef24e5b25f4798a9c55519294619479
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/29eb00db9ddbf891573926a49a39d5406ef24e5b25f4798a9c55519294619479.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 15 witnesses for program sv-benchmarks/c/forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i, 29eb00db9ddbf891573926a49a39d5406ef24e5b25f4798a9c55519294619479
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/29eb00db9ddbf891573926a49a39d5406ef24e5b25f4798a9c55519294619479.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
8398948 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2019-12-01 07:38:30 | ||
4ef31f9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 10 | 2019-12-11T21:09:02+01:00 | 8398948 | |
8d966bd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 10 | 2019-12-06T02:39:39+01:00 | ca32e1f | |
adc1780 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 10 | 2019-12-01T05:05:08+01:00 | ||
cef1c4b | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 9 | 2019-12-08T00:06:51+01:00 | bd28cc5 | |
d9bcd8f | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.9 | 11 | 2019-12-11T21:57:10+01:00 | adc1780 | |
b50ee47 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.9 | 11 | 2019-12-11T20:55:11+01:00 | 1b10dde | |
5355481 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.9 | 11 | 2019-12-05T20:22:05+01:00 | 2787f7c | |
81fc787 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.9 | 11 | 2019-12-03T08:10:32+01:00 | a583423 | |
a583423 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.9 | 10 | 2019-11-30T14:50:53+01:00 | ||
1095477 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 10 | 2019-12-11T20:07:03+01:00 | 580803d | |
1fe3858 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 10 | 2019-12-07T23:47:55+01:00 | 06979c5 | |
f62f66e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 10 | 2019-11-30T17:11:18+01:00 | a99278b | |
a99278b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 10 | 2019-11-30T05:50:02+01:00 | ||
580803d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 10 | 2019-12-01T16:02:42+01:00 |
Found 20 witnesses for program sv-benchmarks/c/forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i, 29eb00db9ddbf891573926a49a39d5406ef24e5b25f4798a9c55519294619479
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/29eb00db9ddbf891573926a49a39d5406ef24e5b25f4798a9c55519294619479.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
67269e9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T08:45 CET (sv-comp) | ||
a72ba60 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-10T10:48:53+01:00 | 9460333 | |
6c766a8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-08T23:42:39+01:00 | 67269e9 | |
7d5b793 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-08T04:07:33+01:00 | 9460333 | |
c5be71b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 11 | 2018-12-08T22:12:15+01:00 | 73f6f28 | |
1490f40 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-06T00:40:34+01:00 | ||
fda2bfe | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-07T09:29:50+01:00 | cbbb27e | |
a5bbfd4 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 10 | 2018-12-07T09:59:07+01:00 | ||
73f6f28 | 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-08T10:10:12 | ||
89b7ee1 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-07T01:09:29+01:00 | 9003771 | |
852bfba | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 11 | 2018-12-08T04:56:42+01:00 | 6c0577d | |
39ce51a | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 11 | 2018-12-06T10:20:34+01:00 | 7b4cbdf | |
f007e45 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 11 | 2018-12-06T09:20:49+01:00 | e89f21d | |
09a2790 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T03:23:03 | ||
40bc85b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 10 | 2018-12-07T08:08:42+01:00 | ||
8fae58a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-08T21:57:38+01:00 | 09a2790 | |
f1d2141 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-08T07:32:15+01:00 | 40bc85b | |
f275315 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-07T08:45:08+01:00 | c42e5be | |
7070e77 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-06T09:00:23+01:00 | 9e49951 | |
9e49951 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-05T11:44:00+01:00 |
Found 16 witnesses for program sv-benchmarks/c/forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i, 29eb00db9ddbf891573926a49a39d5406ef24e5b25f4798a9c55519294619479
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/29eb00db9ddbf891573926a49a39d5406ef24e5b25f4798a9c55519294619479.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c865216 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2017-12-02T23:59 CET (sv-comp) | ||
cbbb27e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | PredatorHP | 4 | 2017-12-01T22:06 CET (sv-comp) | ||
c5bb714 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Map2Check | 3 | 2017-12-01T23:48 CET (sv-comp) | ||
403371f | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 kind | 6 | 2017-12-02T11:00:56.652185 | ||
c06702d | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 incr | 7 | 2017-12-01T23:05:27.484338 | ||
94e3779 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 3.1 | 4 | 2017-12-01T09:34 CET (sv-comp) | ||
e972d16 | 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 | 25 | 2017-12-01T08:21 CET (sv-comp) | ||
864b1ca | 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 | 7 | 2017-12-01T08:20 CET (sv-comp) | ||
cbfcd7e | 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 | 41 | 2017-12-01T19:29 CET (sv-comp) | ||
22dc205 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 9 | 2017-12-01T01:22:22+01:00 | ||
c42e5be | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | PredatorHP | 4 | 2017-12-01T20:28 CET (sv-comp) | ||
dd909ec | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Forester | 40 | 2017-12-01T18:07 CET (sv-comp) | ||
fda3d09 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 10 | 2017-12-01T21:18:42+01:00 | 49cc42f | |
8d5e742 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 10 | 2017-12-01T18:47:18+01:00 | 0b4522e | |
505b644 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 10 | 2017-12-01T05:18:14+01:00 | 96cf2b7 | |
299b07b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 18 | 2017-12-01T02:45:49+01:00 |
Found 0 witnesses for program sv-benchmarks/c/forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i, 29eb00db9ddbf891573926a49a39d5406ef24e5b25f4798a9c55519294619479
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/29eb00db9ddbf891573926a49a39d5406ef24e5b25f4798a9c55519294619479.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |