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

View and Validate the Witness

Input Given to this Service about the Witness (URL Query)

Key Value
programName ../../../comp/sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i
programSHA 5c0b005902832ab9153f2c6eaf0f9a258db7edb3c0998a363eeb94f72f2d77a6
witnessName results-verified/predatorhp.2017-12-01_2024.logfiles/sv-comp18.list_true-unreach-call_false-valid-memtrack.i.files/witness.graphml
witnessSHA c7a0648207e50ebf0fd21000e69978733084558f0b303a726384b722098658d8

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/c7a0648207e50ebf0fd21000e69978733084558f0b303a726384b722098658d8.json

Key Value
architecture 32bit
creationtime 2017-12-01T20:49 CET (sv-comp)
memorymodel precise
producer PredatorHP
program-sha256 5c0b005902832ab9153f2c6eaf0f9a258db7edb3c0998a363eeb94f72f2d77a6
programfile ../../sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i
programhash d10df8dd204379b6ee00f8f6f7d78e7298076c9e
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/c7a0648207e50ebf0fd21000e69978733084558f0b303a726384b722098658d8.graphml
witness-sha256 c7a0648207e50ebf0fd21000e69978733084558f0b303a726384b722098658d8
witness-size 3577
witness-type correctness_witness

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

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

Found 0 witnesses for program ../../../comp/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, ../../../comp/sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program ../../../comp/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, ../../../comp/sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program ../../../comp/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, ../../../comp/sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program ../../../comp/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, ../../../comp/sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program ../../../comp/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, ../../../comp/sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program ../../../comp/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, ../../../comp/sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i).

Found 12 witnesses for program ../../../comp/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, ../../../comp/sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program ../../../comp/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