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/loop-acceleration/nested_true-unreach-call1.i
programSHA bedcacd264f1cd4c2d84284e0ba31f1f477cb1c747be14e67c05106652adf8d0
witnessName results-validated/cpa-seq-validate-correctness-witnesses-viap.2018-12-09_2105.logfiles/sv-comp19_prop-reachsafety.nested_true-unreach-call1.i.files/witness.graphml
witnessSHA b721b46da5badc5c7c9b79f17c687dcc77d705e6dbf2d42e0f489046aee49312

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-09T21:06:26+01:00
inputwitnesshash 59ecf2cab4c300148aa16ae172df157efb64cc9f071330cbe30d543f5ec1c6b0
producer CPAchecker 1.7-svn 29852
program-sha256 bedcacd264f1cd4c2d84284e0ba31f1f477cb1c747be14e67c05106652adf8d0
programfile ../../sv-benchmarks/c/loop-acceleration/nested_true-unreach-call1.i
programhash bedcacd264f1cd4c2d84284e0ba31f1f477cb1c747be14e67c05106652adf8d0
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/b721b46da5badc5c7c9b79f17c687dcc77d705e6dbf2d42e0f489046aee49312.graphml
witness-sha256 b721b46da5badc5c7c9b79f17c687dcc77d705e6dbf2d42e0f489046aee49312
witness-size 5983
witness-type correctness_witness

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

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

Trying to find witnesses for program (bedcacd264f1cd4c2d84284e0ba31f1f477cb1c747be14e67c05106652adf8d0, sv-benchmarks/c/loop-acceleration/nested_true-unreach-call1.i).

Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/nested_true-unreach-call1.i, bedcacd264f1cd4c2d84284e0ba31f1f477cb1c747be14e67c05106652adf8d0
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/bedcacd264f1cd4c2d84284e0ba31f1f477cb1c747be14e67c05106652adf8d0.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 (bedcacd264f1cd4c2d84284e0ba31f1f477cb1c747be14e67c05106652adf8d0, sv-benchmarks/c/loop-acceleration/nested_true-unreach-call1.i).

Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/nested_true-unreach-call1.i, bedcacd264f1cd4c2d84284e0ba31f1f477cb1c747be14e67c05106652adf8d0
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/bedcacd264f1cd4c2d84284e0ba31f1f477cb1c747be14e67c05106652adf8d0.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 (bedcacd264f1cd4c2d84284e0ba31f1f477cb1c747be14e67c05106652adf8d0, sv-benchmarks/c/loop-acceleration/nested_true-unreach-call1.i).

Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/nested_true-unreach-call1.i, bedcacd264f1cd4c2d84284e0ba31f1f477cb1c747be14e67c05106652adf8d0
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/bedcacd264f1cd4c2d84284e0ba31f1f477cb1c747be14e67c05106652adf8d0.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 (bedcacd264f1cd4c2d84284e0ba31f1f477cb1c747be14e67c05106652adf8d0, sv-benchmarks/c/loop-acceleration/nested_true-unreach-call1.i).

Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/nested_true-unreach-call1.i, bedcacd264f1cd4c2d84284e0ba31f1f477cb1c747be14e67c05106652adf8d0
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/bedcacd264f1cd4c2d84284e0ba31f1f477cb1c747be14e67c05106652adf8d0.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 (bedcacd264f1cd4c2d84284e0ba31f1f477cb1c747be14e67c05106652adf8d0, sv-benchmarks/c/loop-acceleration/nested_true-unreach-call1.i).

Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/nested_true-unreach-call1.i, bedcacd264f1cd4c2d84284e0ba31f1f477cb1c747be14e67c05106652adf8d0
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/bedcacd264f1cd4c2d84284e0ba31f1f477cb1c747be14e67c05106652adf8d0.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 (bedcacd264f1cd4c2d84284e0ba31f1f477cb1c747be14e67c05106652adf8d0, sv-benchmarks/c/loop-acceleration/nested_true-unreach-call1.i).

Found 13 witnesses for program sv-benchmarks/c/loop-acceleration/nested_true-unreach-call1.i, bedcacd264f1cd4c2d84284e0ba31f1f477cb1c747be14e67c05106652adf8d0
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/bedcacd264f1cd4c2d84284e0ba31f1f477cb1c747be14e67c05106652adf8d0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7a81ea0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T11:37 CET (sv-comp)
Download be9b32b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 7 2018-12-07T01:01:36+01:00
Download ab281ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-10T20:15:50+01:00 Download 2650472
Download b721b46 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-09T21:06:26+01:00 Download 59ecf2c
Download 5bd0b3e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-09T20:23:38+01:00 Download 0314443
Download 7251eea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-09T17:06:26+01:00 Download fa32c50
Download 30ed862 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T23:07:43+01:00 Download 7a81ea0
Download a8b9989 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T07:03:32+01:00 Download be9b32b
Download 509295b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-07T17:45:56+01:00 Download aa7c08a
Download 4fd8bf3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:28:37+01:00 Download a0734f9
Download a1eb386 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T08:54:29+01:00 Download 2997da2
Download 4434ddc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T08:02:56+01:00 Download 3cd949a
Download 2997da2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-05T10:01:11+01:00

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

Trying to find witnesses for program (bedcacd264f1cd4c2d84284e0ba31f1f477cb1c747be14e67c05106652adf8d0, sv-benchmarks/c/loop-acceleration/nested_true-unreach-call1.i).

Found 16 witnesses for program sv-benchmarks/c/loop-acceleration/nested_true-unreach-call1.i, bedcacd264f1cd4c2d84284e0ba31f1f477cb1c747be14e67c05106652adf8d0
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/bedcacd264f1cd4c2d84284e0ba31f1f477cb1c747be14e67c05106652adf8d0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download aa7c08a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T22:13 CET (sv-comp)
Download b72d77a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 6 2017-12-02T16:49Z
Download 093fe52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T08:04 CET (sv-comp)
Download d0ab707 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 7 2017-12-02T21:58:26+01:00
Download f78ab7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 7 2017-12-01T04:51:50+01:00
Download 8d7aff3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-03T06:51:09+01:00 d9cc67d
Download 48aa38d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-03T04:16:03+01:00 f839de2
Download f245753 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-03T01:02:59+01:00 5644da7
Download 68f4456 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T20:53:38+01:00 f6c7d74
Download 068870f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T00:14:49+01:00 0aed3c6
Download e4214e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T08:14:07+01:00 ef26f91
Download d4b5cad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T05:18:34+01:00 149a360
Download a45d2c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T05:01:47+01:00 5a3bf0f
Download 01c02a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T03:52:42+01:00
Download 2cc0647 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 6 2017-12-02T16:02Z
Download 9b08700 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 9 2017-11-30T12:07 CET (sv-comp)

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

Trying to find witnesses for program (bedcacd264f1cd4c2d84284e0ba31f1f477cb1c747be14e67c05106652adf8d0, sv-benchmarks/c/loop-acceleration/nested_true-unreach-call1.i).

Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/nested_true-unreach-call1.i, bedcacd264f1cd4c2d84284e0ba31f1f477cb1c747be14e67c05106652adf8d0
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/bedcacd264f1cd4c2d84284e0ba31f1f477cb1c747be14e67c05106652adf8d0.json

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