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 (c4f8c014c88e97ce72309926e435d6bbbacd2ef0b94ceb563585756a743fa754, sv-benchmarks/c/list-ext-properties/test-0019_1_false-valid-memtrack_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/list-ext-properties/test-0019_1_false-valid-memtrack_true-termination.i, c4f8c014c88e97ce72309926e435d6bbbacd2ef0b94ceb563585756a743fa754
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/c4f8c014c88e97ce72309926e435d6bbbacd2ef0b94ceb563585756a743fa754.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 (c4f8c014c88e97ce72309926e435d6bbbacd2ef0b94ceb563585756a743fa754, sv-benchmarks/c/list-ext-properties/test-0019_1_false-valid-memtrack_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/list-ext-properties/test-0019_1_false-valid-memtrack_true-termination.i, c4f8c014c88e97ce72309926e435d6bbbacd2ef0b94ceb563585756a743fa754
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/c4f8c014c88e97ce72309926e435d6bbbacd2ef0b94ceb563585756a743fa754.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 (c4f8c014c88e97ce72309926e435d6bbbacd2ef0b94ceb563585756a743fa754, sv-benchmarks/c/list-ext-properties/test-0019_1_false-valid-memtrack_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/list-ext-properties/test-0019_1_false-valid-memtrack_true-termination.i, c4f8c014c88e97ce72309926e435d6bbbacd2ef0b94ceb563585756a743fa754
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/c4f8c014c88e97ce72309926e435d6bbbacd2ef0b94ceb563585756a743fa754.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 (c4f8c014c88e97ce72309926e435d6bbbacd2ef0b94ceb563585756a743fa754, sv-benchmarks/c/list-ext-properties/test-0019_1_false-valid-memtrack_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/list-ext-properties/test-0019_1_false-valid-memtrack_true-termination.i, c4f8c014c88e97ce72309926e435d6bbbacd2ef0b94ceb563585756a743fa754
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/c4f8c014c88e97ce72309926e435d6bbbacd2ef0b94ceb563585756a743fa754.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 (c4f8c014c88e97ce72309926e435d6bbbacd2ef0b94ceb563585756a743fa754, sv-benchmarks/c/list-ext-properties/test-0019_1_false-valid-memtrack_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/list-ext-properties/test-0019_1_false-valid-memtrack_true-termination.i, c4f8c014c88e97ce72309926e435d6bbbacd2ef0b94ceb563585756a743fa754
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/c4f8c014c88e97ce72309926e435d6bbbacd2ef0b94ceb563585756a743fa754.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 '19

Trying to find witnesses for program (c4f8c014c88e97ce72309926e435d6bbbacd2ef0b94ceb563585756a743fa754, sv-benchmarks/c/list-ext-properties/test-0019_1_false-valid-memtrack_true-termination.i).

Found 15 witnesses for program sv-benchmarks/c/list-ext-properties/test-0019_1_false-valid-memtrack_true-termination.i, c4f8c014c88e97ce72309926e435d6bbbacd2ef0b94ceb563585756a743fa754
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/c4f8c014c88e97ce72309926e435d6bbbacd2ef0b94ceb563585756a743fa754.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 81e6f49 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2018-12-08T13:33 CET (sv-comp)
Download 94afa8d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T23:42:14+01:00 Download 81e6f49
Download dc13558 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T08:06:05+01:00 Download 2ecaabf
Download 502ba9b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T04:04:29+01:00 Download 1471ff0
Download 4c8a348 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:42:47+01:00 Download b0740d9
Download 2ecaabf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 6 2018-12-08T00:44:47+01:00
Download bbd1de2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-07T09:30:25+01:00 Download 7d84435
Download 2b43218 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-05T21:39:10+01:00
Download 17c3c94 Inspect Inspect
Validate
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:09:21
Download 6abf677 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-10T10:48:43+01:00 Download 1471ff0
Download aebbf3a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T22:08:51+01:00 Download 17c3c94
Download b48e132 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-07T01:08:16+01:00 Download 718913f
Download fa57395 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:48:21+01:00 Download 2b43218
Download 3c51718 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T01:38 CET (sv-comp)
Download 1ac3c25 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T15:42 CET (sv-comp)

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

Trying to find witnesses for program (c4f8c014c88e97ce72309926e435d6bbbacd2ef0b94ceb563585756a743fa754, sv-benchmarks/c/list-ext-properties/test-0019_1_false-valid-memtrack_true-termination.i).

Found 15 witnesses for program sv-benchmarks/c/list-ext-properties/test-0019_1_false-valid-memtrack_true-termination.i, c4f8c014c88e97ce72309926e435d6bbbacd2ef0b94ceb563585756a743fa754
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/c4f8c014c88e97ce72309926e435d6bbbacd2ef0b94ceb563585756a743fa754.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 2714984 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2017-12-02T23:58 CET (sv-comp)
Download 7d84435 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness PredatorHP 4 2017-12-01T22:06 CET (sv-comp)
Download d675bca Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Map2Check 4 2017-12-01T23:58 CET (sv-comp)
Download 6d0e871 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T08:34:30+01:00
Download a60b42a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T11:55:29.263173
Download e6de115 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T23:09:29.974193
Download 76a1075 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 3.1 4 2017-12-01T09:35 CET (sv-comp)
Download 2757d9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CBMC 17 2017-12-01T08:29 CET (sv-comp)
Download 20d2297 Inspect Inspect
Validate
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:24 CET (sv-comp)
Download 3b7a7c9 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 6 2017-12-01T19:27 CET (sv-comp)
Download 75bcdd0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T20:05:10.728440
Download 08421f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T08:16:10.307348
Download 828f14c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 5 2017-12-01T19:04 CET (sv-comp)
Download a4d8c10 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 8 2017-12-01T16:07 CET (sv-comp)
Download e570d52 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 31 2017-12-01T16:01 CET (sv-comp)

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

Trying to find witnesses for program (c4f8c014c88e97ce72309926e435d6bbbacd2ef0b94ceb563585756a743fa754, sv-benchmarks/c/list-ext-properties/test-0019_1_false-valid-memtrack_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/list-ext-properties/test-0019_1_false-valid-memtrack_true-termination.i, c4f8c014c88e97ce72309926e435d6bbbacd2ef0b94ceb563585756a743fa754
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/c4f8c014c88e97ce72309926e435d6bbbacd2ef0b94ceb563585756a743fa754.json

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