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/memsafety/test-0019_false-valid-memtrack_true-termination.i |
programSHA | 9788c68c1d4dae2d3486d425c7bb2b4d2aac40acd34aea483ac2885cde759917 |
witnessName | results-verified/symbiotic.2017-12-02_2308.logfiles/sv-comp18.test-0019_false-valid-memtrack_true-termination.i.files/witness.graphml |
witnessSHA | 7fd5197293865aab86be080829978e55330c4f192c660a26657c4ffc27aa6b85 |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-02T23:35 CET (sv-comp) |
producer | Symbiotic |
program-sha256 | 9788c68c1d4dae2d3486d425c7bb2b4d2aac40acd34aea483ac2885cde759917 |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_9a3599f7-3d16-43f2-812b-c6b34442165d/sv-benchmarks/c/memsafety/test-0019_false-valid-memtrack_true-termination.i |
programhash | 3e29a7fa8491bc0edf7e32b974ff0e341ea18209 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G valid-memtrack) ) |
witness-file | witnessFileByHash/7fd5197293865aab86be080829978e55330c4f192c660a26657c4ffc27aa6b85.graphml |
witness-sha256 | 7fd5197293865aab86be080829978e55330c4f192c660a26657c4ffc27aa6b85 |
witness-size | 942 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/memsafety/test-0019_false-valid-memtrack_true-termination.i, 9788c68c1d4dae2d3486d425c7bb2b4d2aac40acd34aea483ac2885cde759917
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/9788c68c1d4dae2d3486d425c7bb2b4d2aac40acd34aea483ac2885cde759917.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-0019_false-valid-memtrack_true-termination.i, 9788c68c1d4dae2d3486d425c7bb2b4d2aac40acd34aea483ac2885cde759917
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/9788c68c1d4dae2d3486d425c7bb2b4d2aac40acd34aea483ac2885cde759917.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-0019_false-valid-memtrack_true-termination.i, 9788c68c1d4dae2d3486d425c7bb2b4d2aac40acd34aea483ac2885cde759917
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/9788c68c1d4dae2d3486d425c7bb2b4d2aac40acd34aea483ac2885cde759917.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-0019_false-valid-memtrack_true-termination.i, 9788c68c1d4dae2d3486d425c7bb2b4d2aac40acd34aea483ac2885cde759917
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/9788c68c1d4dae2d3486d425c7bb2b4d2aac40acd34aea483ac2885cde759917.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-0019_false-valid-memtrack_true-termination.i, 9788c68c1d4dae2d3486d425c7bb2b4d2aac40acd34aea483ac2885cde759917
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/9788c68c1d4dae2d3486d425c7bb2b4d2aac40acd34aea483ac2885cde759917.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 15 witnesses for program sv-benchmarks/c/memsafety/test-0019_false-valid-memtrack_true-termination.i, 9788c68c1d4dae2d3486d425c7bb2b4d2aac40acd34aea483ac2885cde759917
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/9788c68c1d4dae2d3486d425c7bb2b4d2aac40acd34aea483ac2885cde759917.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
802c713 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T08:33 CET (sv-comp) | ||
2f7e3e5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 5 | 2018-12-07T12:03:57+01:00 | ||
dda149e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-10T10:48:46+01:00 | 6416061 | |
670d8c7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T23:44:03+01:00 | 802c713 | |
f7a7a54 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T22:10:33+01:00 | 5c193c9 | |
e024a6e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T09:04:25+01:00 | 2f7e3e5 | |
1e13139 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:48:06+01:00 | 9443157 | |
9443157 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-05T15:54:42+01:00 | ||
b296594 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-07T09:16:53+01:00 | 428dc56 | |
5c193c9 | 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-08T13:52:50 | ||
eac9087 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T03:40:44+01:00 | 6416061 | |
2da0513 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-07T01:18:19+01:00 | 9eed047 | |
eac3bec | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:42:16+01:00 | 636fd88 | |
c4b8a13 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T21:05 CET (sv-comp) | ||
faec8d5 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T10:01 CET (sv-comp) |
Found 15 witnesses for program sv-benchmarks/c/memsafety/test-0019_false-valid-memtrack_true-termination.i, 9788c68c1d4dae2d3486d425c7bb2b4d2aac40acd34aea483ac2885cde759917
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/9788c68c1d4dae2d3486d425c7bb2b4d2aac40acd34aea483ac2885cde759917.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7fd5197 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2017-12-02T23:35 CET (sv-comp) | ||
428dc56 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | PredatorHP | 4 | 2017-12-01T22:18 CET (sv-comp) | ||
d11e1c8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Map2Check | 4 | 2017-12-01T23:24 CET (sv-comp) | ||
fdf2044 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-12-01T08:26:02+01:00 | ||
aafff57 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T10:47:59.460700 | ||
ca3aad2 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T23:34:58.065749 | ||
0fa29d0 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 3.1 | 4 | 2017-12-01T09:20 CET (sv-comp) | ||
a2726ee | 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 | 10 | 2017-12-01T08:20 CET (sv-comp) | ||
737948c | 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 | 4 | 2017-12-01T08:21 CET (sv-comp) | ||
b27663f | 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 | 6 | 2017-12-01T19:23 CET (sv-comp) | ||
fd5d101 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-03T00:26:43.826620 | ||
8119a47 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T10:36:09.617948 | ||
a666482 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 5 | 2017-12-01T20:41 CET (sv-comp) | ||
bd3ef1c | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 8 | 2017-12-01T17:18 CET (sv-comp) | ||
d899d57 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 28 | 2017-12-01T13:26 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/memsafety/test-0019_false-valid-memtrack_true-termination.i, 9788c68c1d4dae2d3486d425c7bb2b4d2aac40acd34aea483ac2885cde759917
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/9788c68c1d4dae2d3486d425c7bb2b4d2aac40acd34aea483ac2885cde759917.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |