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/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i
programSHA 920aa3d88a91d3b89885f6dfba09bdbb0aa993f607ac334eff5308d8f0a569ee
witnessName results-verified/ukojak.2018-12-08_1104.logfiles/sv-comp19_prop-reachsafety.verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i.files/witness.graphml
witnessSHA b0ac952c603d96d6c1dfcbd68d3930f6b3a1eb22403e21a944f0f901fb9e1b49

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-09T17:49Z
producer Kojak
programfile /tmp/vcloud-vcloud-master/worker/working_dir_8fc20ddc-fbbf-4ce4-a97c-bf4022f4bc44/sv-benchmarks/c/loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i
programhash 5f5357e64289d6bac41f74df7b40a85eebbaa806
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/b0ac952c603d96d6c1dfcbd68d3930f6b3a1eb22403e21a944f0f901fb9e1b49.graphml
witness-sha256 b0ac952c603d96d6c1dfcbd68d3930f6b3a1eb22403e21a944f0f901fb9e1b49
witness-size 13478
witness-type violation_witness

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

Trying to find witnesses for program (920aa3d88a91d3b89885f6dfba09bdbb0aa993f607ac334eff5308d8f0a569ee, sv-benchmarks/c/loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i).

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

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

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

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

Found 11 witnesses for program sv-benchmarks/c/loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i, 920aa3d88a91d3b89885f6dfba09bdbb0aa993f607ac334eff5308d8f0a569ee
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/920aa3d88a91d3b89885f6dfba09bdbb0aa993f607ac334eff5308d8f0a569ee.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b6eb097 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 25 2019-12-11T21:57:57+01:00 Download ba19129
Download d01c9e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 16 2019-12-11T21:47:20+01:00 Download b678d83
Download 71d2c4b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 16 2019-12-11T20:54:37+01:00 Download 9f95c77
Download 646963c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 16 2019-12-08T01:51:57+01:00 Download d198014
Download ab3726b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 25 2019-12-08T00:27:26+01:00 Download fae0ee1
Download 8caad5b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 25 2019-12-07T21:16:46+01:00 Download 0479d20
Download 9981d30 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 16 2019-12-03T08:03:09+01:00 Download f071ac3
Download f071ac3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 14 2019-11-29T15:29:38+01:00
Download d198014 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 15 2019-12-07T22:29:19+01:00
Download b678d83 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 15 2019-12-01T01:53:58+01:00
Download 69685c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T23:22 CET (comp)

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

Trying to find witnesses for program (920aa3d88a91d3b89885f6dfba09bdbb0aa993f607ac334eff5308d8f0a569ee, sv-benchmarks/c/loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i).

Found 15 witnesses for program sv-benchmarks/c/loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i, 920aa3d88a91d3b89885f6dfba09bdbb0aa993f607ac334eff5308d8f0a569ee
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/920aa3d88a91d3b89885f6dfba09bdbb0aa993f607ac334eff5308d8f0a569ee.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f66f036 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 5 2018-12-08T06:20:34
Download 4854b2a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 10 2018-12-07T00:19 CET (sv-comp)
Download b44bade Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 14 2018-12-10T17:07:18+01:00
Download 68feafe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 15 2018-12-06T20:53:03+01:00
Download 5985afd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-10T20:38:01+01:00 Download b44bade
Download 00b0c74 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 25 2018-12-09T20:24:13+01:00 Download b0ac952
Download cc10803 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-08T07:51:34+01:00 Download 68feafe
Download 20fdf93 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-08T05:05:40+01:00 Download 00635fb
Download 4795a83 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 17 2018-12-07T17:43:00+01:00 Download 4854b2a
Download f922856 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-06T10:18:42+01:00 Download d1b8e4a
Download 3b56d40 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-06T09:48:07+01:00 Download 8dbf4f0
Download f700c1b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 22 2018-12-06T09:18:40+01:00 Download f8403c2
Download 00b351b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 17 2018-12-06T09:14:10+01:00 Download 00ae23e
Download 8dbf4f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-06T03:06:41+01:00
Download 57a0b7b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T07:56 CET (sv-comp)

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

Trying to find witnesses for program (920aa3d88a91d3b89885f6dfba09bdbb0aa993f607ac334eff5308d8f0a569ee, sv-benchmarks/c/loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i, 920aa3d88a91d3b89885f6dfba09bdbb0aa993f607ac334eff5308d8f0a569ee
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/920aa3d88a91d3b89885f6dfba09bdbb0aa993f607ac334eff5308d8f0a569ee.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 '17

Trying to find witnesses for program (920aa3d88a91d3b89885f6dfba09bdbb0aa993f607ac334eff5308d8f0a569ee, sv-benchmarks/c/loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i).

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

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