Witness Inspection

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).

This link does not point to a witness, but below is a list of witnesses for the same program.

Available Results for the Program from Witness Store SV-COMP '24

Trying to find witnesses for program (e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51, sv-benchmarks/c/ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c).

Found 27 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c, e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e9efd80 Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2023-12-18T10:20:15+01:00
Download 041d1a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2023-11-29T18:59:56Z
Download 245ae04 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 3 2023-11-30T04:38:38+01:00
Download 0601c30 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 3 2023-12-03T20:17:25+01:00
Download e880c56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 3 2023-12-18T23:55:14+01:00
Download a3179c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 3 2023-12-18T02:17:47+01:00
Download 2c0b806 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-05T07:36:06Z
Download 0b8e412 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-04T12:29:14Z
Download 0bfae32 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-01T20:02:10Z
Download 27e3838 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 7.4.0 incr 3 2023-12-01T10:26:21Z
Download 0169406 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Taipan 23 2023-12-02T14:36:50Z
Download b314a80 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness PredatorHP 4 2023-11-30T08:26:07Z
Download 293221d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Mopsa (v1.0~pre2) 3 2023-11-29T06:38:59Z
Download 5b6e74b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Kojak 23 2023-12-02T22:41:52Z
Download cef44c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 4 2023-12-01T01:03:14Z
Download d110896 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CBMC 5 2023-12-17T12:01:54+01:00
Download d258cd0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Automizer 23 2023-11-29T04:56:18Z
Download 6e90faa Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness 2LS 4 2023-11-30T22:50:56+01:00
Download 5cb7ada Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 7.4.0 3 2023-12-01T14:02:51Z
Download a90921c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2023-11-29T20:07:14Z
Download 78d0a6f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2023-12-19T23:45:54
Download 770c848 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 3 2023-12-01T02:05:01Z
Download d5d2b3a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 5 2023-12-17T16:37:55+01:00
Download af94e10 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-05T10:00:38Z
Download fc7ca16 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-04T14:31:11Z
Download 37e7e2b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-01T19:56:51Z
Download 7992dd6 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 4 2023-11-30T22:02:56+01:00

Available Results for the Program from Witness Store SV-COMP '23

Trying to find witnesses for program (e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51, sv-benchmarks/c/ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c).

Found 21 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c, e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f7303e3 Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2022-12-09T06:22:04+01:00
Download 3f40954 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 3 2022-12-10T15:37:11+01:00
Download dd138cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 3 2022-12-11T20:56:16+01:00
Download b9d0b47 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 3 2022-12-09T23:31:39+01:00
Download 23f243d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 3 2022-12-09T03:13:03+01:00
Download a6388d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2022-12-08T15:36:47Z
Download 6d47fb9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 7.0.0 incr 3 2022-12-18T16:32:52Z
Download 4d32285 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 6.8.0 incr 3 2022-12-25T11:25:45Z
Download 8119b86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Taipan 23 2022-12-14T09:04:31Z
Download 1fa035b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Mopsa (v1.0~pre2) 3 2022-12-11T11:22:25Z
Download 3f278aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Kojak 23 2022-12-15T01:44:15Z
Download 022d6aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CBMC 5 2022-12-08T11:12:33+01:00
Download a50ed84 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Automizer 23 2022-12-13T20:49:03Z
Download f549780 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness 2LS 4 2022-12-08T02:14:20+01:00
Download 8512e3f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(reach_error())) ) correctness_witness ESBMC 6.8.0 3 2022-12-25T10:37:19Z
Download af5a4ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 7.0.0 3 2022-12-19T01:34:28Z
Download ffc54dd Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2022-12-12T14:32:58Z
Download 2cc5b3e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2022-12-11T17:34:40
Download 23e3ef0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 5 2022-12-08T11:28:54+01:00
Download 1ff743f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2022-12-08T15:19:37Z
Download 40efcc8 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 4 2022-12-07T21:52:18+01:00

Available Results for the Program from Witness Store SV-COMP '22

Trying to find witnesses for program (e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51, sv-benchmarks/c/ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c).

Found 17 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c, e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 75ec76d Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2021-12-07T10:00:15+01:00
Download 4a43e04 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 3 2021-12-05T15:01:58+01:00
Download f3c684e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 3 2021-12-08T20:32:45+01:00
Download 02aced6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 3 2021-12-07T03:34:06+01:00
Download 3b9da73 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 6.8.0 incr 3 2021-12-08T09:12:41Z
Download 74688f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Taipan 23 2021-12-10T04:53:11Z
Download fef9828 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Kojak 23 2021-12-10T10:47:02Z
Download bf215e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CBMC 3 2021-12-06T08:07:32+01:00
Download 5411388 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Automizer 23 2021-12-06T17:34:43Z
Download bc77e47 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness 2LS 4 2021-12-05T23:14:28+01:00
Download 7d16372 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness SESL 2 2021-12-06T11:27:24+01:00
Download 2199b41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 3 2021-12-09T11:52:33+01:00
Download 20aab09 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(reach_error())) ) correctness_witness ESBMC 6.8.0 3 2021-12-08T03:49:50Z
Download 1c31f60 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2021-12-07T17:21:01Z
Download f912c58 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2021-12-09T06:08:18
Download b7dc191 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 3 2021-12-06T05:32:11+01:00
Download 43b40df Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 4 2021-12-05T22:29:52+01:00

Available Results for the Program from Witness Store SV-COMP '21

Trying to find witnesses for program (e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51, sv-benchmarks/c/ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c).

Found 6 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c, e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 79742d7 Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2020-12-06T17:52:45+01:00
Download 0a929e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 3 2020-12-07T23:58:33+01:00
Download f4637de Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 2.0 3 2020-12-05T14:09:09+01:00
Download a005e64 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-11T15:38:15
Download d0a61a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-08T18:56:03
Download 2701eaa Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2020-12-08T08:26:48

Available Results for the Program from Witness Store SV-COMP '20

Trying to find witnesses for program (e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51, sv-benchmarks/c/ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c).

Found 3 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c, e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download db3c971 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 3 2019-11-30T23:43:03+01:00
Download 3a4f7c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.9 3 2019-11-30T03:12:37+01:00
Download 659a351 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T01:19 CET (comp)

Available Results for the Program from Witness Store SV-COMP '19

Trying to find witnesses for program (e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51, sv-benchmarks/c/ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c).

Found 5 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c, e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download efd7275 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 1 2018-12-08T07:46 CET (sv-comp)
Download eec99ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 3 2018-12-06T21:58:51+01:00
Download d05d2af Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-06T05:00:25+01:00
Download aa2b8ff Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T13:46 CET (sv-comp)
Download 407400f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T11:21 CET (sv-comp)

Available Results for the Program from Witness Store SV-COMP '18

Trying to find witnesses for program (e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51, sv-benchmarks/c/ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c).

Found 17 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c, e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3eb86d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 1 2017-12-02T23:31 CET (sv-comp)
Download 9c0e8b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.6.1-svn 26773 3 2017-12-01T08:32:28+01:00
Download 64d817a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-02T10:42:49.465765
Download 6a26bb7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T23:53:22.113451
Download 9ed580d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.6.1-svn 5 2017-12-01T09:14:46+01:00
Download b319768 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Taipan 3 2017-12-03T06:55Z
Download 36d9abc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Map2Check 2 2017-12-01T23:12 CET (sv-comp)
Download f276e94 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Kojak 3 2017-12-03T03:59Z
Download 014e0e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Forester 4 2017-12-01T19:46 CET (sv-comp)
Download 6004a54 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CBMC 3 2017-12-01T08:27 CET (sv-comp)
Download 14ec756 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Automizer 3 2017-12-03T03:57Z
Download aae3d60 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness 2LS 4 2017-12-01T08:19 CET (sv-comp)
Download 38c42e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T20:09:30.860063
Download ef73797 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T12:56:38.137781
Download c5b72d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 4 2017-12-01T19:49 CET (sv-comp)
Download cd13b13 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 3 2017-12-01T16:35 CET (sv-comp)
Download 1fe0475 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 4 2017-12-01T12:56 CET (sv-comp)

Available Results for the Program from Witness Store SV-COMP '17

Trying to find witnesses for program (e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51, sv-benchmarks/c/ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c, e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness