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 (641e22b7eb5566175a3a6b4b63ce4cf70b6f16d8b73e0b01e6faba1efdbc59ea, sv-benchmarks/c/list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i).

Found 0 witnesses for program sv-benchmarks/c/list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i, 641e22b7eb5566175a3a6b4b63ce4cf70b6f16d8b73e0b01e6faba1efdbc59ea
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/641e22b7eb5566175a3a6b4b63ce4cf70b6f16d8b73e0b01e6faba1efdbc59ea.json

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

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

Trying to find witnesses for program (641e22b7eb5566175a3a6b4b63ce4cf70b6f16d8b73e0b01e6faba1efdbc59ea, sv-benchmarks/c/list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i).

Found 0 witnesses for program sv-benchmarks/c/list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i, 641e22b7eb5566175a3a6b4b63ce4cf70b6f16d8b73e0b01e6faba1efdbc59ea
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/641e22b7eb5566175a3a6b4b63ce4cf70b6f16d8b73e0b01e6faba1efdbc59ea.json

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

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

Trying to find witnesses for program (641e22b7eb5566175a3a6b4b63ce4cf70b6f16d8b73e0b01e6faba1efdbc59ea, sv-benchmarks/c/list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i).

Found 0 witnesses for program sv-benchmarks/c/list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i, 641e22b7eb5566175a3a6b4b63ce4cf70b6f16d8b73e0b01e6faba1efdbc59ea
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/641e22b7eb5566175a3a6b4b63ce4cf70b6f16d8b73e0b01e6faba1efdbc59ea.json

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

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

Trying to find witnesses for program (641e22b7eb5566175a3a6b4b63ce4cf70b6f16d8b73e0b01e6faba1efdbc59ea, sv-benchmarks/c/list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i).

Found 0 witnesses for program sv-benchmarks/c/list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i, 641e22b7eb5566175a3a6b4b63ce4cf70b6f16d8b73e0b01e6faba1efdbc59ea
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/641e22b7eb5566175a3a6b4b63ce4cf70b6f16d8b73e0b01e6faba1efdbc59ea.json

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

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

Trying to find witnesses for program (641e22b7eb5566175a3a6b4b63ce4cf70b6f16d8b73e0b01e6faba1efdbc59ea, sv-benchmarks/c/list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i).

Found 17 witnesses for program sv-benchmarks/c/list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i, 641e22b7eb5566175a3a6b4b63ce4cf70b6f16d8b73e0b01e6faba1efdbc59ea
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/641e22b7eb5566175a3a6b4b63ce4cf70b6f16d8b73e0b01e6faba1efdbc59ea.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 704080e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.9 13 2019-11-30T05:11:52+01:00
Download 2300413 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 13 2019-11-30T21:01:17+01:00
Download c9a19c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-04T00:26 CET (comp)
Download bff38aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 13 2019-12-11T20:37:34+01:00 Download 47b69a5
Download 894bb7f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 13 2019-12-11T20:22:27+01:00 Download 3a49bc9
Download 1a9b4d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 13 2019-12-11T20:17:48+01:00 Download df5ad84
Download 9004e98 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 13 2019-12-08T01:01:05+01:00 Download a8a1b94
Download 58e64e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 13 2019-12-08T00:00:17+01:00 Download 566a1ca
Download 09fd89c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 13 2019-12-07T19:57:07+01:00 Download 07b63e0
Download 93299a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 13 2019-12-06T01:52:50+01:00 Download 263d178
Download c43baed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 13 2019-12-05T19:27:53+01:00 Download b11ac84
Download 0896ae0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 13 2019-12-04T02:22:39+01:00 Download c9a19c6
Download 2f0c889 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 13 2019-11-30T20:10:04+01:00 Download abda7bd
Download 462c50c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 13 2019-11-30T16:25:52+01:00 Download 29d7053
Download 29d7053 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 15 2019-11-30T10:56:50+01:00
Download a8a1b94 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 14 2019-12-07T14:18:19+01:00
Download 3a49bc9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 13 2019-12-01T00:13:57+01:00

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

Trying to find witnesses for program (641e22b7eb5566175a3a6b4b63ce4cf70b6f16d8b73e0b01e6faba1efdbc59ea, sv-benchmarks/c/list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i).

Found 22 witnesses for program sv-benchmarks/c/list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i, 641e22b7eb5566175a3a6b4b63ce4cf70b6f16d8b73e0b01e6faba1efdbc59ea
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/641e22b7eb5566175a3a6b4b63ce4cf70b6f16d8b73e0b01e6faba1efdbc59ea.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b6f86ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 1 2018-12-08T19:55 CET (sv-comp)
Download a65ab4d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 13 2018-12-08T03:51:14+01:00
Download 2277236 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-05T15:50:52+01:00
Download e78879d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T19:31 CET (sv-comp)
Download 9cf8ec1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T00:49:41
Download a40a77f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T01:17 CET (sv-comp)
Download 1838b2e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7 14 2018-12-10T18:12:26+01:00
Download 5e2f87e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 16 2018-12-06T23:40:17+01:00
Download 1c79408 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-10T19:43:22+01:00 Download 1838b2e
Download 773ad8a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-10T10:30:43+01:00 Download ca035bf
Download d09ce9a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-08T23:24:10+01:00 Download e78879d
Download 674dfba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-08T21:38:44+01:00 Download 9cf8ec1
Download fb49f7a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-08T06:10:01+01:00 Download 5e2f87e
Download 2a4737b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-08T03:57:21+01:00 Download 7fc4891
Download c46ff72 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-08T02:00:13+01:00 Download ca035bf
Download 25a879e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-07T16:39:27+01:00 Download a40a77f
Download 46d390c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-07T08:52:55+01:00 Download 659f6a8
Download 6984984 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-06T09:28:23+01:00 Download 66d4346
Download 82a92a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-06T08:45:32+01:00 Download dbe8880
Download a080b66 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-06T08:24:22+01:00 Download 6cbe021
Download 459b902 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-06T08:23:17+01:00 Download 6b3e0f0
Download dbe8880 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 15 2018-12-05T20:10:19+01:00

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

Trying to find witnesses for program (641e22b7eb5566175a3a6b4b63ce4cf70b6f16d8b73e0b01e6faba1efdbc59ea, sv-benchmarks/c/list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i).

Found 0 witnesses for program sv-benchmarks/c/list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i, 641e22b7eb5566175a3a6b4b63ce4cf70b6f16d8b73e0b01e6faba1efdbc59ea
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/641e22b7eb5566175a3a6b4b63ce4cf70b6f16d8b73e0b01e6faba1efdbc59ea.json

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

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

Trying to find witnesses for program (641e22b7eb5566175a3a6b4b63ce4cf70b6f16d8b73e0b01e6faba1efdbc59ea, sv-benchmarks/c/list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i).

Found 0 witnesses for program sv-benchmarks/c/list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i, 641e22b7eb5566175a3a6b4b63ce4cf70b6f16d8b73e0b01e6faba1efdbc59ea
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/641e22b7eb5566175a3a6b4b63ce4cf70b6f16d8b73e0b01e6faba1efdbc59ea.json

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