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 (2a3b30ff739d918a6dda0d427a3dbd5889d24dc079d2a03cff70cfe8d9a13ae9, sv-benchmarks/c/list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i).

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

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

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

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

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

Found 0 witnesses for program sv-benchmarks/c/list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i, 2a3b30ff739d918a6dda0d427a3dbd5889d24dc079d2a03cff70cfe8d9a13ae9
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/2a3b30ff739d918a6dda0d427a3dbd5889d24dc079d2a03cff70cfe8d9a13ae9.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 (2a3b30ff739d918a6dda0d427a3dbd5889d24dc079d2a03cff70cfe8d9a13ae9, sv-benchmarks/c/list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i).

Found 18 witnesses for program sv-benchmarks/c/list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i, 2a3b30ff739d918a6dda0d427a3dbd5889d24dc079d2a03cff70cfe8d9a13ae9
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/2a3b30ff739d918a6dda0d427a3dbd5889d24dc079d2a03cff70cfe8d9a13ae9.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 68f7348 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2017-12-03T00:11 CET (sv-comp)
Download e0c8813 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T10:40:26.852006
Download c4d45b7 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:10:14.910993
Download d6a75e8 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 fb3157a 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 Taipan 9 2017-12-03T06:54Z
Download 81ca1eb 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 Kojak 9 2017-12-03T04:02Z
Download f02d58a 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 Forester 6 2017-12-01T19:40 CET (sv-comp)
Download 9ed806d 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 12 2017-12-01T08:23 CET (sv-comp)
Download 817e456 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 Automizer 9 2017-12-03T03:57Z
Download d527b2d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness PredatorHP 4 2017-12-01T22:12 CET (sv-comp)
Download afbda00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Map2Check 2 2017-12-01T23:44 CET (sv-comp)
Download 121a03f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T11:00 CET (sv-comp)
Download 2dcd3b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 8 2017-12-01T20:59 CET (sv-comp)
Download a7569df Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Forester 6 2017-12-01T18:21 CET (sv-comp)
Download 53b8c06 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 16 2017-12-02T01:47:33.842669
Download 356614b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 17 2017-12-01T20:56:38.145538
Download a2c82a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 8 2017-12-01T06:17 CET (sv-comp)
Download d4cf671 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 8 2017-12-01T01:28 CET (sv-comp)

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

Trying to find witnesses for program (2a3b30ff739d918a6dda0d427a3dbd5889d24dc079d2a03cff70cfe8d9a13ae9, sv-benchmarks/c/list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i).

Found 0 witnesses for program sv-benchmarks/c/list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i, 2a3b30ff739d918a6dda0d427a3dbd5889d24dc079d2a03cff70cfe8d9a13ae9
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/2a3b30ff739d918a6dda0d427a3dbd5889d24dc079d2a03cff70cfe8d9a13ae9.json

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