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/underapprox_true-unreach-call2_true-termination.i
programSHA 0c24d96206a617343af24f81991fab503d9e4386a14e97fa4c8c900b9cb61b43
witnessName results-validated/cpa-seq-validate-correctness-witnesses-veriabs.2018-12-10_1933.logfiles/sv-comp19_prop-reachsafety.underapprox_true-unreach-call2_true-termination.i.files/witness.graphml
witnessSHA 46262063c999b95fb81a2318f3e8a51593c9d07cf400a38141847f9581ce646b

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-10T19:47:46+01:00
inputwitnesshash 0144065207546dec277ae02960b0d27fe40c04c3d8dd7a9beffa21b93c7fc0a1
producer CPAchecker 1.7-svn 29852
program-sha256 0c24d96206a617343af24f81991fab503d9e4386a14e97fa4c8c900b9cb61b43
programfile ../../sv-benchmarks/c/loop-acceleration/underapprox_true-unreach-call2_true-termination.i
programhash 0c24d96206a617343af24f81991fab503d9e4386a14e97fa4c8c900b9cb61b43
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/46262063c999b95fb81a2318f3e8a51593c9d07cf400a38141847f9581ce646b.graphml
witness-sha256 46262063c999b95fb81a2318f3e8a51593c9d07cf400a38141847f9581ce646b
witness-size 5049
witness-type correctness_witness

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

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

Trying to find witnesses for program (0c24d96206a617343af24f81991fab503d9e4386a14e97fa4c8c900b9cb61b43, sv-benchmarks/c/loop-acceleration/underapprox_true-unreach-call2_true-termination.i).

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

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

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

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

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

Found 25 witnesses for program sv-benchmarks/c/loop-acceleration/underapprox_true-unreach-call2_true-termination.i, 0c24d96206a617343af24f81991fab503d9e4386a14e97fa4c8c900b9cb61b43
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/0c24d96206a617343af24f81991fab503d9e4386a14e97fa4c8c900b9cb61b43.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ae44316 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T03:07 CET (sv-comp)
Download c28bb0c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T05:31:49
Download 3b608ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T10:28 CET (sv-comp)
Download d99f76f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-07T02:57:16+01:00
Download 4626206 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-10T19:47:46+01:00 Download 0144065
Download 30b76e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-10T10:31:19+01:00 Download 3dad41b
Download 302b34f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T21:06:24+01:00 Download db6f9f3
Download 034ec0c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:31:18+01:00 Download 010c468
Download d4d45d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T19:57:49+01:00 Download 6aaf600
Download 190a3a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T17:23:25+01:00 Download 87b20a2
Download b2bb443 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T23:23:23+01:00 Download ae44316
Download 18e3d73 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T21:44:04+01:00 Download c28bb0c
Download d8af347 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T05:30:42+01:00 Download d99f76f
Download a358f97 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T03:40:45+01:00 Download 88f8811
Download e9b6b66 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T02:13:12+01:00 Download 3dad41b
Download 02a8148 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-07T17:45:04+01:00 Download 828f281
Download 2f589a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-07T16:37:34+01:00 Download 3b608ce
Download 9facf45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:28:25+01:00 Download f42dcad
Download 5cd6684 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:00:08+01:00 Download 4084a3c
Download dbde45d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T08:21:58+01:00 Download 4af102a
Download 01daa71 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T07:41:13+01:00 Download ba656b2
Download 582401d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T07:05:33+01:00 Download 4d20f32
Download 4084a3c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-05T18:57:08+01:00
Download ce32f82 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T02:42 CET (sv-comp)
Download 7fa7482 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T01:04 CET (sv-comp)

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

Trying to find witnesses for program (0c24d96206a617343af24f81991fab503d9e4386a14e97fa4c8c900b9cb61b43, sv-benchmarks/c/loop-acceleration/underapprox_true-unreach-call2_true-termination.i).

Found 37 witnesses for program sv-benchmarks/c/loop-acceleration/underapprox_true-unreach-call2_true-termination.i, 0c24d96206a617343af24f81991fab503d9e4386a14e97fa4c8c900b9cb61b43
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/0c24d96206a617343af24f81991fab503d9e4386a14e97fa4c8c900b9cb61b43.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 828f281 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T23:10 CET (sv-comp)
Download 8975d7a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 5 2017-12-02T23:36Z
Download b2faf98 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T07:41 CET (sv-comp)
Download 1d6f8c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 3 2017-12-01T19:49 CET (sv-comp)
Download 604fb2c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 5 2017-12-02T15:37Z
Download 4222426 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T23:36:38.728613
Download 4face1c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T09:13:32.048351
Download 33189b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T15:17:07.062100
Download ed4c902 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T13:50:36.073694
Download a995801 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 5 2017-12-01T15:53 CET (sv-comp)
Download cde6d54 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 6 2017-12-02T23:10:33+01:00
Download 1eb0206 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-11-30T18:05:03+01:00
Download e1ea5be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T06:51:00+01:00 e336052
Download cd66d5e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T04:03:36+01:00 9247ab4
Download 2b8ebfb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-03T03:02:35+01:00 42d00d4
Download e7595b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T01:53:15+01:00 64de4cf
Download c19494e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T20:35:07+01:00 76bd606
Download f965723 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T15:12:07+01:00 c0b6abe
Download dcbd0a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T08:13:25+01:00 8dd44a1
Download 250ebb6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T00:09:23+01:00 ad0232d
Download 5cf80aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T22:33:17+01:00 28e07a9
Download ee5c922 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T22:04:46+01:00 1ecc1eb
Download 3b17788 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T08:13:36+01:00 b241df5
Download 430eff3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T06:43:18+01:00 05a193c
Download 91dcaae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T06:15:57+01:00 4f969d9
Download c5c0674 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T05:23:34+01:00 96cc42c
Download 53ec489 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T05:13:08+01:00 cee7989
Download 92e7060 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T04:34:03+01:00 1e0bc43
Download a54f1e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T01:56:46+01:00
Download 9cfcef5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 8 2017-11-30T18:17:25+01:00
Download 3bc7ce2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 5 2017-11-30T14:02:24+01:00
Download 8b19adf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 5 2017-12-02T09:23:18+01:00
Download a6199ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 9 2017-11-30T11:54 CET (sv-comp)
Download 602543a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 5 2017-12-02T18:09Z
Download 3efbcc6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 9 2017-12-01T02:01 CET (sv-comp)
Download 8a5e264 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 9 2017-12-01T13:14 CET (sv-comp)
Download cc142bf Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 9 2017-12-01T14:08 CET (sv-comp)

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

Trying to find witnesses for program (0c24d96206a617343af24f81991fab503d9e4386a14e97fa4c8c900b9cb61b43, sv-benchmarks/c/loop-acceleration/underapprox_true-unreach-call2_true-termination.i).

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

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