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-crafted/simple_array_index_value_true-unreach-call1_true-termination.i
programSHA 811ccbdeb6332dadd30cb6b65bbd863079d6b0765ac81fa6ea189a8362c52700
witnessName results-verified/cbmc.2018-12-04_2248.logfiles/sv-comp19_prop-reachsafety.simple_array_index_value_true-unreach-call1_true-termination.i.files/witness.graphml
witnessSHA 3e33d785067e72d2363776f3380c624cf0a058cd9cead90d816003f9081b78a0

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-05T12:49 CET (sv-comp)
producer CBMC
programfile ../../sv-benchmarks/c/loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i
programhash ee6e0f96ee2d8c1f99e23755f1e64cdcfbd7f79f
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/3e33d785067e72d2363776f3380c624cf0a058cd9cead90d816003f9081b78a0.graphml
witness-sha256 3e33d785067e72d2363776f3380c624cf0a058cd9cead90d816003f9081b78a0
witness-size 2136220
witness-type correctness_witness

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

Trying to find witnesses for program (811ccbdeb6332dadd30cb6b65bbd863079d6b0765ac81fa6ea189a8362c52700, sv-benchmarks/c/loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i).

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

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

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

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

Found 12 witnesses for program sv-benchmarks/c/loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i, 811ccbdeb6332dadd30cb6b65bbd863079d6b0765ac81fa6ea189a8362c52700
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/811ccbdeb6332dadd30cb6b65bbd863079d6b0765ac81fa6ea189a8362c52700.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c92b8a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-04T00:14 CET (comp)
Download 5df9983 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-11T20:21:15+01:00 Download c44cd85
Download 2704aa0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-11T20:10:22+01:00 Download e72be52
Download 5dc91c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-11T20:04:57+01:00 Download 4771b9d
Download 9349b7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-08T00:59:40+01:00 Download 3e5f21d
Download dd35a8c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-06T01:57:23+01:00 Download f390726
Download cb0c2bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-05T19:16:09+01:00 Download 2b4f3b3
Download bc020f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-04T02:09:49+01:00 Download c92b8a3
Download 06b1646 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-11-30T19:57:10+01:00 Download 466eb5d
Download cf4d4e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-11-30T17:13:44+01:00 Download 117fc4f
Download 117fc4f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 21 2019-11-30T14:11:34+01:00
Download e72be52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 64 2019-12-01T19:41:56+01:00

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

Trying to find witnesses for program (811ccbdeb6332dadd30cb6b65bbd863079d6b0765ac81fa6ea189a8362c52700, sv-benchmarks/c/loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i).

Found 13 witnesses for program sv-benchmarks/c/loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i, 811ccbdeb6332dadd30cb6b65bbd863079d6b0765ac81fa6ea189a8362c52700
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/811ccbdeb6332dadd30cb6b65bbd863079d6b0765ac81fa6ea189a8362c52700.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 836e671 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T04:02 CET (sv-comp)
Download dad56d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T03:57 CET (sv-comp)
Download ab6e56a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 64 2018-12-08T03:14:16+01:00
Download af6c074 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-10T20:28:46+01:00 Download fc5a15e
Download 089f6f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-10T10:46:15+01:00 Download ab3662a
Download 6034b7a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-09T21:21:26+01:00 Download ff4fdc4
Download 1b18878 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-08T23:30:57+01:00 Download 836e671
Download 5e5696b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 26 2018-12-08T07:00:26+01:00 Download ab6e56a
Download 60b023f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-08T03:28:35+01:00 Download 261841b
Download 43ba395 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-08T02:26:46+01:00 Download ab3662a
Download f120541 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-07T16:53:54+01:00 Download dad56d7
Download 7f7267f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T08:22:55+01:00 Download 3e33d78
Download d238d02 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 26 2018-12-05T10:08:21+01:00

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

Trying to find witnesses for program (811ccbdeb6332dadd30cb6b65bbd863079d6b0765ac81fa6ea189a8362c52700, sv-benchmarks/c/loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i).

Found 11 witnesses for program sv-benchmarks/c/loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i, 811ccbdeb6332dadd30cb6b65bbd863079d6b0765ac81fa6ea189a8362c52700
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/811ccbdeb6332dadd30cb6b65bbd863079d6b0765ac81fa6ea189a8362c52700.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 119900f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T03:10 CET (sv-comp)
Download 0b796e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 4 2017-12-01T20:28 CET (sv-comp)
Download 502b62f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T14:26:24.829658
Download 19ba7f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T10:46:52.044480
Download 3a666a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.12-svcomp17 4 2017-11-02T13:16:17+05:30
Download 0c58b7c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-03T04:38:22+01:00 16a47d2
Download 064ba98 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-02T20:46:07+01:00 b443ef4
Download 383817f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-02T08:06:37+01:00 19c44d7
Download 0c81b5c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T22:47:49+01:00 941c4b6
Download ee134e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T22:34:12+01:00 0748591
Download 80eb1b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 2130 2017-12-01T01:48 CET (sv-comp)

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

Trying to find witnesses for program (811ccbdeb6332dadd30cb6b65bbd863079d6b0765ac81fa6ea189a8362c52700, sv-benchmarks/c/loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i, 811ccbdeb6332dadd30cb6b65bbd863079d6b0765ac81fa6ea189a8362c52700
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/811ccbdeb6332dadd30cb6b65bbd863079d6b0765ac81fa6ea189a8362c52700.json

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