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/loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i
programSHA d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8
witnessName results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i.files/witness.graphml
witnessSHA 903c7df336f7d067cd934ae5dd5d790eecb366c62d1019f748ac5a290b17b9d2

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-11-30T11:53:25+01:00
producer CPAchecker 1.6.1-svn 26725
program-sha256 d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8
programfile ../../sv-benchmarks/c/loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i
programhash 10cc4caffca660fca2e6a4a0cd5f7ba7ba4e10af
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/903c7df336f7d067cd934ae5dd5d790eecb366c62d1019f748ac5a290b17b9d2.graphml
witness-sha256 903c7df336f7d067cd934ae5dd5d790eecb366c62d1019f748ac5a290b17b9d2
witness-size 13608
witness-type correctness_witness

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

Trying to find witnesses for program (d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8, sv-benchmarks/c/loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i, d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8.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 (d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8, sv-benchmarks/c/loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i, d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8.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 (d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8, sv-benchmarks/c/loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i, d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8.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 (d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8, sv-benchmarks/c/loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i, d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8.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 (d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8, sv-benchmarks/c/loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i, d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8.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 (d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8, sv-benchmarks/c/loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i, d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8.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 (d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8, sv-benchmarks/c/loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i).

Found 34 witnesses for program sv-benchmarks/c/loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i, d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3db7b4f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 23 2017-12-03T05:17Z
Download 2ca7eef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T05:44 CET (sv-comp)
Download b3c4137 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 5 2017-12-01T21:00 CET (sv-comp)
Download 9d3f137 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 24 2017-12-02T02:30Z
Download 48ba2d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T22:22:31.422790
Download 9053f36 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T08:40:29.084997
Download 8ad6ed1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-02T03:02:45.795493
Download 302efbe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T08:36:39.191314
Download 95706b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 77 2017-12-01T17:40 CET (sv-comp)
Download 1d64ad7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 15 2017-12-03T03:19:47+01:00
Download aa4d670 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-01T05:07:23+01:00
Download fe60d3f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-03T06:51:29+01:00 114d676
Download a16fffe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 14 2017-12-03T04:19:36+01:00 2294215
Download 2a43ff8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-03T01:56:40+01:00 2d93330
Download 8a21fe7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-03T00:52:34+01:00 9acf203
Download d05bf39 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-02T19:53:56+01:00 d281c1e
Download 2e35a6e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-02T15:28:33+01:00 f6d1cac
Download bcfcba1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-02T08:58:54+01:00 9f05720
Download 72d153f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-01T22:21:39+01:00 487eb9d
Download 971db9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-01T22:04:46+01:00 257c0f6
Download 3811cce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-01T08:13:34+01:00 2fbd5d7
Download f33d1fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-01T06:20:53+01:00 d0616d6
Download e92fa20 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-01T05:45:12+01:00 d13112e
Download e30005e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 14 2017-12-01T05:42:41+01:00 b30f955
Download 558563b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-01T05:08:51+01:00 8caace8
Download 21b1c9a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-01T05:00:49+01:00 ea52582
Download 6418ae3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-11-30T15:11:11+01:00
Download 40c6516 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 18 2017-11-30T17:13:50+01:00
Download 903c7df Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 14 2017-11-30T11:53:25+01:00
Download 0c7c179 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 13 2017-12-01T22:22:33+01:00
Download d887739 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 255 2017-11-30T17:15 CET (sv-comp)
Download 3b45f89 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 23 2017-12-02T02:59Z
Download 183a8c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 29 2017-11-30T20:38 CET (sv-comp)
Download e08dba0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 252 2017-12-01T15:24 CET (sv-comp)

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

Trying to find witnesses for program (d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8, sv-benchmarks/c/loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i, d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8.json

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