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/ldv-memsafety/memleaks_test5_true-valid-memsafety_true-termination.i |
programSHA | f53e5d9cc620103fcf03061ce8afcd5598f8aa44cae64bdbfefe8239cbdff35f |
witnessName | results-verified/cpa-seq.2017-12-01_0822.logfiles/sv-comp18.memleaks_test5_true-valid-memsafety_true-termination.i.files/witness.graphml |
witnessSHA | 03cd5b2460994b641ce8e4b74847c871f02ef2bdc814a845bab42c009173a695 |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-01T08:30:47+01:00 |
producer | CPAchecker 1.6.1-svn 26773 |
program-sha256 | f53e5d9cc620103fcf03061ce8afcd5598f8aa44cae64bdbfefe8239cbdff35f |
programfile | ../../sv-benchmarks/c/ldv-memsafety/memleaks_test5_true-valid-memsafety_true-termination.i |
programhash | 69a450466ef894dfd523cea1e8c68b55495b15f9 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G valid-memtrack) ) |
witness-file | witnessFileByHash/03cd5b2460994b641ce8e4b74847c871f02ef2bdc814a845bab42c009173a695.graphml |
witness-sha256 | 03cd5b2460994b641ce8e4b74847c871f02ef2bdc814a845bab42c009173a695 |
witness-size | 14473 |
witness-type | correctness_witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test5_true-valid-memsafety_true-termination.i, f53e5d9cc620103fcf03061ce8afcd5598f8aa44cae64bdbfefe8239cbdff35f
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/f53e5d9cc620103fcf03061ce8afcd5598f8aa44cae64bdbfefe8239cbdff35f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test5_true-valid-memsafety_true-termination.i, f53e5d9cc620103fcf03061ce8afcd5598f8aa44cae64bdbfefe8239cbdff35f
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/f53e5d9cc620103fcf03061ce8afcd5598f8aa44cae64bdbfefe8239cbdff35f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test5_true-valid-memsafety_true-termination.i, f53e5d9cc620103fcf03061ce8afcd5598f8aa44cae64bdbfefe8239cbdff35f
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/f53e5d9cc620103fcf03061ce8afcd5598f8aa44cae64bdbfefe8239cbdff35f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test5_true-valid-memsafety_true-termination.i, f53e5d9cc620103fcf03061ce8afcd5598f8aa44cae64bdbfefe8239cbdff35f
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/f53e5d9cc620103fcf03061ce8afcd5598f8aa44cae64bdbfefe8239cbdff35f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test5_true-valid-memsafety_true-termination.i, f53e5d9cc620103fcf03061ce8afcd5598f8aa44cae64bdbfefe8239cbdff35f
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/f53e5d9cc620103fcf03061ce8afcd5598f8aa44cae64bdbfefe8239cbdff35f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 5 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test5_true-valid-memsafety_true-termination.i, f53e5d9cc620103fcf03061ce8afcd5598f8aa44cae64bdbfefe8239cbdff35f
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/f53e5d9cc620103fcf03061ce8afcd5598f8aa44cae64bdbfefe8239cbdff35f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
4f9ff02 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T02:07 CET (sv-comp) | ||
aff0454 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 15 | 2018-12-07T13:14:30+01:00 | ||
7bbf972 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-06T03:35:00+01:00 | ||
d1d17f9 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T04:36 CET (sv-comp) | ||
7f3918d | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T12:21 CET (sv-comp) |
Found 16 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test5_true-valid-memsafety_true-termination.i, f53e5d9cc620103fcf03061ce8afcd5598f8aa44cae64bdbfefe8239cbdff35f
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/f53e5d9cc620103fcf03061ce8afcd5598f8aa44cae64bdbfefe8239cbdff35f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c82a9a8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T23:11 CET (sv-comp) | ||
03cd5b2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 14 | 2017-12-01T08:30:47+01:00 | ||
4f8c260 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T11:16:23.418166 | ||
68bdc6e | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T23:00:56.791704 | ||
249b7af | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 3.1 | 5 | 2017-12-01T09:39 CET (sv-comp) | ||
ab9d43d | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Taipan | 8 | 2017-12-03T06:54Z | ||
1cf0444 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Map2Check | 4 | 2017-12-01T23:52 CET (sv-comp) | ||
ea6974f | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Kojak | 7 | 2017-12-03T04:14Z | ||
1a142de | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CBMC | 6 | 2017-12-01T08:19 CET (sv-comp) | ||
25c3f43 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Automizer | 8 | 2017-12-03T04:24Z | ||
ae078b8 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | 2LS | 23 | 2017-12-01T08:19 CET (sv-comp) | ||
7446e72 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T23:13:17.444367 | ||
704e30f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T11:22:02.992588 | ||
82c4211 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 5 | 2017-12-01T15:53 CET (sv-comp) | ||
8b6c09f | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 6 | 2017-12-01T17:46 CET (sv-comp) | ||
122548a | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 23 | 2017-12-01T15:23 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test5_true-valid-memsafety_true-termination.i, f53e5d9cc620103fcf03061ce8afcd5598f8aa44cae64bdbfefe8239cbdff35f
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/f53e5d9cc620103fcf03061ce8afcd5598f8aa44cae64bdbfefe8239cbdff35f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |