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 (5c0b005902832ab9153f2c6eaf0f9a258db7edb3c0998a363eeb94f72f2d77a6, sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i, 5c0b005902832ab9153f2c6eaf0f9a258db7edb3c0998a363eeb94f72f2d77a6
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/5c0b005902832ab9153f2c6eaf0f9a258db7edb3c0998a363eeb94f72f2d77a6.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 (5c0b005902832ab9153f2c6eaf0f9a258db7edb3c0998a363eeb94f72f2d77a6, sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i, 5c0b005902832ab9153f2c6eaf0f9a258db7edb3c0998a363eeb94f72f2d77a6
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/5c0b005902832ab9153f2c6eaf0f9a258db7edb3c0998a363eeb94f72f2d77a6.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 (5c0b005902832ab9153f2c6eaf0f9a258db7edb3c0998a363eeb94f72f2d77a6, sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i, 5c0b005902832ab9153f2c6eaf0f9a258db7edb3c0998a363eeb94f72f2d77a6
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/5c0b005902832ab9153f2c6eaf0f9a258db7edb3c0998a363eeb94f72f2d77a6.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 (5c0b005902832ab9153f2c6eaf0f9a258db7edb3c0998a363eeb94f72f2d77a6, sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i, 5c0b005902832ab9153f2c6eaf0f9a258db7edb3c0998a363eeb94f72f2d77a6
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/5c0b005902832ab9153f2c6eaf0f9a258db7edb3c0998a363eeb94f72f2d77a6.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 (5c0b005902832ab9153f2c6eaf0f9a258db7edb3c0998a363eeb94f72f2d77a6, sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i, 5c0b005902832ab9153f2c6eaf0f9a258db7edb3c0998a363eeb94f72f2d77a6
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/5c0b005902832ab9153f2c6eaf0f9a258db7edb3c0998a363eeb94f72f2d77a6.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 (5c0b005902832ab9153f2c6eaf0f9a258db7edb3c0998a363eeb94f72f2d77a6, sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i, 5c0b005902832ab9153f2c6eaf0f9a258db7edb3c0998a363eeb94f72f2d77a6
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/5c0b005902832ab9153f2c6eaf0f9a258db7edb3c0998a363eeb94f72f2d77a6.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 '18

Trying to find witnesses for program (5c0b005902832ab9153f2c6eaf0f9a258db7edb3c0998a363eeb94f72f2d77a6, sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i).

Found 12 witnesses for program sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i, 5c0b005902832ab9153f2c6eaf0f9a258db7edb3c0998a363eeb94f72f2d77a6
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/5c0b005902832ab9153f2c6eaf0f9a258db7edb3c0998a363eeb94f72f2d77a6.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 31e82d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2017-12-02T23:12 CET (sv-comp)
Download 6daecb2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness PredatorHP 4 2017-12-01T21:51 CET (sv-comp)
Download 95bcabf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Map2Check 3 2017-12-01T23:37 CET (sv-comp)
Download f90c30d 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:12:18.157654
Download 8d1929d 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:23:58.413049
Download 60f003d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 3.1 4 2017-12-01T09:36 CET (sv-comp)
Download 3a46178 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 26 2017-12-01T08:25 CET (sv-comp)
Download b4b4eac 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 5 2017-12-01T08:19 CET (sv-comp)
Download c7a0648 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness PredatorHP 4 2017-12-01T20:49 CET (sv-comp)
Download ee5303a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-01T21:18:54+01:00 12d0049
Download 0900752 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-01T06:00:15+01:00 7631703
Download bf9233b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 13 2017-11-30T20:32:25+01:00

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

Trying to find witnesses for program (5c0b005902832ab9153f2c6eaf0f9a258db7edb3c0998a363eeb94f72f2d77a6, sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i, 5c0b005902832ab9153f2c6eaf0f9a258db7edb3c0998a363eeb94f72f2d77a6
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/5c0b005902832ab9153f2c6eaf0f9a258db7edb3c0998a363eeb94f72f2d77a6.json

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