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/multivar_false-unreach-call1_true-termination.i
programSHA 2bdc9a65a13a5d2813f156a626a154c13db0d816e947494bb3187b79c7541fc9
witnessName results-validated/cpa-seq-validate-violation-witnesses-cpa-seq.2018-12-06_0944.logfiles/sv-comp19_prop-reachsafety.multivar_false-unreach-call1_true-termination.i.files/witness.graphml
witnessSHA 2ab7d0c3cf47a59c6a32989e59a3a426c402a3534ec112f8ed3097def13cdae6

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-06T09:47:56+01:00
inputwitnesshash 4e4892dd9f3b59347131cd8dcfeb4db1eaf4d65d2b4d50ef4dd6aea95e0e4960
producer CPAchecker 1.7-svn 29852
program-sha256 2bdc9a65a13a5d2813f156a626a154c13db0d816e947494bb3187b79c7541fc9
programfile ../../sv-benchmarks/c/loop-acceleration/multivar_false-unreach-call1_true-termination.i
programhash 2bdc9a65a13a5d2813f156a626a154c13db0d816e947494bb3187b79c7541fc9
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/2ab7d0c3cf47a59c6a32989e59a3a426c402a3534ec112f8ed3097def13cdae6.graphml
witness-sha256 2ab7d0c3cf47a59c6a32989e59a3a426c402a3534ec112f8ed3097def13cdae6
witness-size 5495
witness-type violation_witness

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

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

Trying to find witnesses for program (2bdc9a65a13a5d2813f156a626a154c13db0d816e947494bb3187b79c7541fc9, sv-benchmarks/c/loop-acceleration/multivar_false-unreach-call1_true-termination.i).

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

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

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

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

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

Found 25 witnesses for program sv-benchmarks/c/loop-acceleration/multivar_false-unreach-call1_true-termination.i, 2bdc9a65a13a5d2813f156a626a154c13db0d816e947494bb3187b79c7541fc9
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/2bdc9a65a13a5d2813f156a626a154c13db0d816e947494bb3187b79c7541fc9.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6460379 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T19:06 CET (sv-comp)
Download e411a6a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T12:09:39
Download 1a46d46 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 5 2018-12-07T09:50 CET (sv-comp)
Download bb90f64 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 5 2018-12-10T17:29:07+01:00
Download 9b7068e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-07T13:14:34+01:00
Download 1fb665d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-10T20:36:44+01:00 Download bb90f64
Download 9e215d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:53:08+01:00 Download cabc6b2
Download 2da2fbf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:35:45+01:00 Download 263531c
Download 9e48f53 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:21:00+01:00 Download 2485e6f
Download b8586a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T18:21:51+01:00 Download 59bdb28
Download 652fe52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 1262 2018-12-08T23:42:09+01:00 Download 6460379
Download 1002b0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T22:08:55+01:00 Download e411a6a
Download 362b26a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T08:40:14+01:00 Download 9b7068e
Download 91182a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T04:51:56+01:00 Download 3cc6cd7
Download 7ac3e6b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T04:06:35+01:00 Download db6a031
Download b475cbc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-07T18:48:12+01:00 Download f7bd0e8
Download 32106b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-07T17:45:45+01:00 Download 1a46d46
Download f7d3351 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T10:19:11+01:00 Download 7730469
Download 2ab7d0c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:47:56+01:00 Download 4e4892d
Download 995b03b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:41:59+01:00 Download 7cfcf2d
Download abf796e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:15:00+01:00 Download 3088340
Download 714d59c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:00:21+01:00 Download ff71d30
Download 4e4892d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T07:53:57+01:00
Download cc9afe0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-07T01:11:31+01:00 Download eb87320
Download 73d0541 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T04:33 CET (sv-comp)

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

Trying to find witnesses for program (2bdc9a65a13a5d2813f156a626a154c13db0d816e947494bb3187b79c7541fc9, sv-benchmarks/c/loop-acceleration/multivar_false-unreach-call1_true-termination.i).

Found 21 witnesses for program sv-benchmarks/c/loop-acceleration/multivar_false-unreach-call1_true-termination.i, 2bdc9a65a13a5d2813f156a626a154c13db0d816e947494bb3187b79c7541fc9
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/2bdc9a65a13a5d2813f156a626a154c13db0d816e947494bb3187b79c7541fc9.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 4de8945 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 3 2017-12-01T23:11 CET (sv-comp)
Download 845e09a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 5 2017-12-03T03:32Z
Download fe8c74b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T07:17 CET (sv-comp)
Download d56622e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 2 2017-12-01T20:23 CET (sv-comp)
Download 1144f13 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 5 2017-12-02T20:30Z
Download 20c1af6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T19:44:08.835896
Download e506865 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T18:27:46.221593
Download 00b8df8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 4 2017-12-01T18:19 CET (sv-comp)
Download 595d2da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 4 2017-12-01T05:09 CET (sv-comp)
Download 30cb179 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 6 2017-12-03T02:34:45+01:00
Download 028d475 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-11-30T15:59:37+01:00
Download b65293e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 8 2017-11-30T15:19:44+01:00
Download fb9cc96 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 5 2017-11-30T13:50:27+01:00
Download 67dcfe6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 5 2017-12-01T19:19:15+01:00
Download 811ce5d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 5 2017-11-30T22:37 CET (sv-comp)
Download 409f554 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 5 2017-12-02T20:18Z
Download 7cfcf2d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 4 2017-12-01T03:32 CET (sv-comp)
Download 511fecf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T01:07:58.362198
Download 5786458 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T14:43:35.784395
Download 3effa78 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 957 2017-12-01T17:14 CET (sv-comp)
Download 7734c2b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 9 2017-12-01T15:20 CET (sv-comp)

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

Trying to find witnesses for program (2bdc9a65a13a5d2813f156a626a154c13db0d816e947494bb3187b79c7541fc9, sv-benchmarks/c/loop-acceleration/multivar_false-unreach-call1_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/multivar_false-unreach-call1_true-termination.i, 2bdc9a65a13a5d2813f156a626a154c13db0d816e947494bb3187b79c7541fc9
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/2bdc9a65a13a5d2813f156a626a154c13db0d816e947494bb3187b79c7541fc9.json

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