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-ext-properties/960521-1_1_false-valid-deref.i |
programSHA | ccd495816ca97f890203673d93e17687bdaa095f05835da8b9df24aac18cb803 |
witnessName | results-verified/symbiotic.2018-12-07_2142.logfiles/sv-comp19_prop-memsafety.960521-1_1_false-valid-deref.i.files/witness.graphml |
witnessSHA | 1c296abb4f1095c37b406c56984e38e335d620c97344a3621ed6e3a21c72f6ea |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-08T02:52 CET (sv-comp) |
producer | Symbiotic |
program-sha256 | ccd495816ca97f890203673d93e17687bdaa095f05835da8b9df24aac18cb803 |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_bc9dfc79-30c9-432b-9374-9d8c58d0e924/sv-benchmarks/c/list-ext-properties/960521-1_1_false-valid-deref.i |
programhash | ccd495816ca97f890203673d93e17687bdaa095f05835da8b9df24aac18cb803 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G valid-memtrack) ) |
witness-file | witnessFileByHash/1c296abb4f1095c37b406c56984e38e335d620c97344a3621ed6e3a21c72f6ea.graphml |
witness-sha256 | 1c296abb4f1095c37b406c56984e38e335d620c97344a3621ed6e3a21c72f6ea |
witness-size | 957 |
witness-type | violation_witness |
This witness was created for this program (cf. table above, ccd495816ca97f890203673d93e17687bdaa095f05835da8b9df24aac18cb803).
Found 0 witnesses for program sv-benchmarks/c/list-ext-properties/960521-1_1_false-valid-deref.i, ccd495816ca97f890203673d93e17687bdaa095f05835da8b9df24aac18cb803
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/ccd495816ca97f890203673d93e17687bdaa095f05835da8b9df24aac18cb803.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/list-ext-properties/960521-1_1_false-valid-deref.i, ccd495816ca97f890203673d93e17687bdaa095f05835da8b9df24aac18cb803
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/ccd495816ca97f890203673d93e17687bdaa095f05835da8b9df24aac18cb803.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/list-ext-properties/960521-1_1_false-valid-deref.i, ccd495816ca97f890203673d93e17687bdaa095f05835da8b9df24aac18cb803
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/ccd495816ca97f890203673d93e17687bdaa095f05835da8b9df24aac18cb803.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/list-ext-properties/960521-1_1_false-valid-deref.i, ccd495816ca97f890203673d93e17687bdaa095f05835da8b9df24aac18cb803
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/ccd495816ca97f890203673d93e17687bdaa095f05835da8b9df24aac18cb803.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/list-ext-properties/960521-1_1_false-valid-deref.i, ccd495816ca97f890203673d93e17687bdaa095f05835da8b9df24aac18cb803
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/ccd495816ca97f890203673d93e17687bdaa095f05835da8b9df24aac18cb803.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 19 witnesses for program sv-benchmarks/c/list-ext-properties/960521-1_1_false-valid-deref.i, ccd495816ca97f890203673d93e17687bdaa095f05835da8b9df24aac18cb803
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/ccd495816ca97f890203673d93e17687bdaa095f05835da8b9df24aac18cb803.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
1c296ab | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T02:52 CET (sv-comp) | ||
79c7e00 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-10T10:48:59+01:00 | 82c4f4e | |
b6bf806 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 90 | 2018-12-08T08:40:20+01:00 | 4ea5285 | |
86b4805 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-08T04:14:34+01:00 | 82c4f4e | |
ca5d14c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 90 | 2018-12-06T09:48:39+01:00 | b5b5797 | |
b5b5797 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 109 | 2018-12-05T12:09:12+01:00 | ||
743b113 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T10:18:14+01:00 | 8fbb89f | |
2f46462 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T09:10:47+01:00 | 48b2c02 | |
547e4b8 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-07T09:25:05+01:00 | 6916b45 | |
42c5a41 | 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 | 4 | 2018-12-08T09:19:56 | ||
4ea5285 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 109 | 2018-12-06T21:13:07+01:00 | ||
729e03f | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-09T20:53:12+01:00 | 7965470 | |
a8a904f | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-09T20:36:36+01:00 | 0b4ed73 | |
18ba886 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-09T20:28:30+01:00 | efde685 | |
8d3fa69 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-08T23:44:29+01:00 | 1c296ab | |
164bf38 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-07T01:06:06+01:00 | 5cf1109 | |
9726049 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-08T22:10:52+01:00 | 42c5a41 | |
b9676e7 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T04:54:00+01:00 | 3d49bf0 | |
48c52d8 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T09:12:42+01:00 | e506299 |
Found 12 witnesses for program sv-benchmarks/c/list-ext-properties/960521-1_1_false-valid-deref.i, ccd495816ca97f890203673d93e17687bdaa095f05835da8b9df24aac18cb803
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/ccd495816ca97f890203673d93e17687bdaa095f05835da8b9df24aac18cb803.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
5bd0611 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2017-12-03T00:01 CET (sv-comp) | ||
564fa03 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T11:00:42.967817 | ||
5671b9e | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 incr | 5 | 2017-12-01T23:24:54.251167 | ||
1d72adc | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 3.1 | 5 | 2017-12-01T09:31 CET (sv-comp) | ||
873d69a | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Taipan | 8 | 2017-12-03T06:58Z | ||
6522c81 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Kojak | 8 | 2017-12-03T04:21Z | ||
99d053b | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Forester | 4 | 2017-12-01T19:39 CET (sv-comp) | ||
8a03fdd | 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 | 7 | 2017-12-01T08:31 CET (sv-comp) | ||
7369867 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Automizer | 8 | 2017-12-03T04:00Z | ||
6916b45 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | PredatorHP | 4 | 2017-12-01T22:13 CET (sv-comp) | ||
ce8ff6d | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Map2Check | 2 | 2017-12-01T23:16 CET (sv-comp) | ||
91e6bfd | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 106 | 2017-12-01T08:28:54+01:00 |
Found 0 witnesses for program sv-benchmarks/c/list-ext-properties/960521-1_1_false-valid-deref.i, ccd495816ca97f890203673d93e17687bdaa095f05835da8b9df24aac18cb803
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/ccd495816ca97f890203673d93e17687bdaa095f05835da8b9df24aac18cb803.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |