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 sv-benchmarks/c/list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i
programSHA 76e7f02297fe04629e411e42e1076fc13482ba963645870c0b367c7465680776
witnessName results-validated/cpa-seq-validate-violation-witnesses-map2check.2018-12-07_0102.logfiles/sv-comp19_prop-memsafety.list-ext_flag_false-unreach-call_false-valid-deref.i.files/witness.graphml
witnessSHA de74d9183b66c2b0c374bacc9525087e9a79e4092612d52ab93d003d2ec6a39b

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/de74d9183b66c2b0c374bacc9525087e9a79e4092612d52ab93d003d2ec6a39b.json

Key Value
architecture 32bit
creationtime 2018-12-07T01:08:09+01:00
inputwitnesshash 7fcc44f5178c1e688487d28474bcc0c427c969a137957555caff78f1a41c557c
producer CPAchecker 1.7-svn 29852
program-sha256 76e7f02297fe04629e411e42e1076fc13482ba963645870c0b367c7465680776
programfile ../../sv-benchmarks/c/list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i
programhash 76e7f02297fe04629e411e42e1076fc13482ba963645870c0b367c7465680776
sourcecodelang C
specification CHECK( init(main()), LTL(G valid-deref) )
witness-file witnessFileByHash/de74d9183b66c2b0c374bacc9525087e9a79e4092612d52ab93d003d2ec6a39b.graphml
witness-sha256 de74d9183b66c2b0c374bacc9525087e9a79e4092612d52ab93d003d2ec6a39b
witness-size 8076
witness-type violation_witness

This witness was created for this program (cf. table above, 76e7f02297fe04629e411e42e1076fc13482ba963645870c0b367c7465680776).

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

Trying to find witnesses for program (76e7f02297fe04629e411e42e1076fc13482ba963645870c0b367c7465680776, 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, 76e7f02297fe04629e411e42e1076fc13482ba963645870c0b367c7465680776
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/76e7f02297fe04629e411e42e1076fc13482ba963645870c0b367c7465680776.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 (76e7f02297fe04629e411e42e1076fc13482ba963645870c0b367c7465680776, 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, 76e7f02297fe04629e411e42e1076fc13482ba963645870c0b367c7465680776
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/76e7f02297fe04629e411e42e1076fc13482ba963645870c0b367c7465680776.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 (76e7f02297fe04629e411e42e1076fc13482ba963645870c0b367c7465680776, 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, 76e7f02297fe04629e411e42e1076fc13482ba963645870c0b367c7465680776
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/76e7f02297fe04629e411e42e1076fc13482ba963645870c0b367c7465680776.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 (76e7f02297fe04629e411e42e1076fc13482ba963645870c0b367c7465680776, 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, 76e7f02297fe04629e411e42e1076fc13482ba963645870c0b367c7465680776
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/76e7f02297fe04629e411e42e1076fc13482ba963645870c0b367c7465680776.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 (76e7f02297fe04629e411e42e1076fc13482ba963645870c0b367c7465680776, 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, 76e7f02297fe04629e411e42e1076fc13482ba963645870c0b367c7465680776
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/76e7f02297fe04629e411e42e1076fc13482ba963645870c0b367c7465680776.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 (76e7f02297fe04629e411e42e1076fc13482ba963645870c0b367c7465680776, sv-benchmarks/c/list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i).

Found 20 witnesses for program sv-benchmarks/c/list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i, 76e7f02297fe04629e411e42e1076fc13482ba963645870c0b367c7465680776
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/76e7f02297fe04629e411e42e1076fc13482ba963645870c0b367c7465680776.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 52f8fa5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-09T20:36:45+01:00 Download 12ef1c3
Download 1a60a72 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-09T20:21:48+01:00 Download ed76152
Download fd386db Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T10:19:01+01:00 Download 718168b
Download 2bff9b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 11 2018-12-06T13:43:08+01:00
Download 79a7103 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-08T05:04:45+01:00 Download 482f40a
Download 4045f6f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-06T09:21:27+01:00 Download 93399f4
Download 228193b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-05T15:21:48+01:00
Download 9276305 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-07T09:16:36+01:00 Download 535ce33
Download 4a4c2ed 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-08T17:25:21
Download 2de81d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-09T20:53:15+01:00 Download c88a840
Download de74d91 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-07T01:08:09+01:00 Download 7fcc44f
Download 1a66c6a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-08T22:10:18+01:00 Download 4a4c2ed
Download bae4734 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T00:57 CET (sv-comp)
Download d20775a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 8 2018-12-08T11:06:00
Download ed37e7b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 79 2018-12-07T14:29 CET (sv-comp)
Download 5fa81f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 78 2018-12-07T04:28:54+01:00
Download 34bab15 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 77 2018-12-08T07:57:15+01:00 Download 5fa81f3
Download ff0aae1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-07T17:30:27+01:00 Download ed37e7b
Download ab45b40 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 18 2018-12-06T09:49:12+01:00 Download 758c088
Download 758c088 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 33 2018-12-05T22:31:35+01:00

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

Trying to find witnesses for program (76e7f02297fe04629e411e42e1076fc13482ba963645870c0b367c7465680776, 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, 76e7f02297fe04629e411e42e1076fc13482ba963645870c0b367c7465680776
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/76e7f02297fe04629e411e42e1076fc13482ba963645870c0b367c7465680776.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 (76e7f02297fe04629e411e42e1076fc13482ba963645870c0b367c7465680776, 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, 76e7f02297fe04629e411e42e1076fc13482ba963645870c0b367c7465680776
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/76e7f02297fe04629e411e42e1076fc13482ba963645870c0b367c7465680776.json

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