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/bitvector-loops/diamond_false-unreach-call2.i
programSHA bcf679bfa04b1fbcd635d39b7fcf10b90f13b5b1b9a6cb34d9f932caed50dbe3
witnessName results-verified/uautomizer.2018-12-08_0742.logfiles/sv-comp19_prop-reachsafety.diamond_false-unreach-call2.i.files/witness.graphml
witnessSHA befd8047dfea672634d673d2fdeec028efd278b52c3e86f180164f4133ea3e6f

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-09T09:33Z
producer Automizer
programfile /tmp/vcloud-vcloud-master/worker/working_dir_ae723b86-41c4-44a9-b27f-349763e4c153/sv-benchmarks/c/bitvector-loops/diamond_false-unreach-call2.i
programhash dee4f98e3deb83265bbf70c3b5c0f3c1ff37b06c
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/befd8047dfea672634d673d2fdeec028efd278b52c3e86f180164f4133ea3e6f.graphml
witness-sha256 befd8047dfea672634d673d2fdeec028efd278b52c3e86f180164f4133ea3e6f
witness-size 13281
witness-type violation_witness

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

Trying to find witnesses for program (bcf679bfa04b1fbcd635d39b7fcf10b90f13b5b1b9a6cb34d9f932caed50dbe3, sv-benchmarks/c/bitvector-loops/diamond_false-unreach-call2.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector-loops/diamond_false-unreach-call2.i, bcf679bfa04b1fbcd635d39b7fcf10b90f13b5b1b9a6cb34d9f932caed50dbe3
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/bcf679bfa04b1fbcd635d39b7fcf10b90f13b5b1b9a6cb34d9f932caed50dbe3.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 (bcf679bfa04b1fbcd635d39b7fcf10b90f13b5b1b9a6cb34d9f932caed50dbe3, sv-benchmarks/c/bitvector-loops/diamond_false-unreach-call2.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector-loops/diamond_false-unreach-call2.i, bcf679bfa04b1fbcd635d39b7fcf10b90f13b5b1b9a6cb34d9f932caed50dbe3
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/bcf679bfa04b1fbcd635d39b7fcf10b90f13b5b1b9a6cb34d9f932caed50dbe3.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 (bcf679bfa04b1fbcd635d39b7fcf10b90f13b5b1b9a6cb34d9f932caed50dbe3, sv-benchmarks/c/bitvector-loops/diamond_false-unreach-call2.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector-loops/diamond_false-unreach-call2.i, bcf679bfa04b1fbcd635d39b7fcf10b90f13b5b1b9a6cb34d9f932caed50dbe3
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/bcf679bfa04b1fbcd635d39b7fcf10b90f13b5b1b9a6cb34d9f932caed50dbe3.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 (bcf679bfa04b1fbcd635d39b7fcf10b90f13b5b1b9a6cb34d9f932caed50dbe3, sv-benchmarks/c/bitvector-loops/diamond_false-unreach-call2.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector-loops/diamond_false-unreach-call2.i, bcf679bfa04b1fbcd635d39b7fcf10b90f13b5b1b9a6cb34d9f932caed50dbe3
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/bcf679bfa04b1fbcd635d39b7fcf10b90f13b5b1b9a6cb34d9f932caed50dbe3.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 (bcf679bfa04b1fbcd635d39b7fcf10b90f13b5b1b9a6cb34d9f932caed50dbe3, sv-benchmarks/c/bitvector-loops/diamond_false-unreach-call2.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector-loops/diamond_false-unreach-call2.i, bcf679bfa04b1fbcd635d39b7fcf10b90f13b5b1b9a6cb34d9f932caed50dbe3
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/bcf679bfa04b1fbcd635d39b7fcf10b90f13b5b1b9a6cb34d9f932caed50dbe3.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 (bcf679bfa04b1fbcd635d39b7fcf10b90f13b5b1b9a6cb34d9f932caed50dbe3, sv-benchmarks/c/bitvector-loops/diamond_false-unreach-call2.i).

Found 24 witnesses for program sv-benchmarks/c/bitvector-loops/diamond_false-unreach-call2.i, bcf679bfa04b1fbcd635d39b7fcf10b90f13b5b1b9a6cb34d9f932caed50dbe3
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/bcf679bfa04b1fbcd635d39b7fcf10b90f13b5b1b9a6cb34d9f932caed50dbe3.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c86797d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T00:46 CET (sv-comp)
Download e9cfc8b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 6 2018-12-08T05:23:55
Download cece911 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 10 2018-12-07T02:46 CET (sv-comp)
Download 0e8773b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 14 2018-12-10T18:53:53+01:00
Download 3645ec2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 14 2018-12-07T04:08:03+01:00
Download 356e7f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-10T20:35:36+01:00 Download 0e8773b
Download c1141ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-09T20:53:16+01:00 Download 6a403a8
Download c076ded Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-09T20:39:05+01:00 Download befd804
Download 2e61be5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-09T20:23:06+01:00 Download a65ccd9
Download 4982cc0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-09T18:21:05+01:00 Download a18e350
Download 660a1ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-08T23:44:15+01:00 Download c86797d
Download 8f3caa0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-08T22:09:51+01:00 Download e9cfc8b
Download 424268b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-08T08:22:43+01:00 Download 3645ec2
Download b5e24ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-08T05:05:07+01:00 Download 067ad9e
Download 4472bd1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-08T04:34:12+01:00 Download 26095eb
Download d1c5115 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-07T18:46:25+01:00 Download 4b713e0
Download 2c20ef3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-07T17:43:33+01:00 Download cece911
Download dbd5b33 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-06T10:17:37+01:00 Download 39dbdf2
Download 26febf0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-06T09:48:46+01:00 Download 7a9a49f
Download 1f073b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-06T09:20:12+01:00 Download 2ab1645
Download 7a9a49f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-06T04:30:23+01:00
Download 3693783 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-07T01:16:57+01:00 Download e8d941c
Download 10ee96f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-06T09:40:31+01:00 Download 6c6d4dd
Download a95dce6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-06T09:00:23+01:00 Download 276e77d

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

Trying to find witnesses for program (bcf679bfa04b1fbcd635d39b7fcf10b90f13b5b1b9a6cb34d9f932caed50dbe3, sv-benchmarks/c/bitvector-loops/diamond_false-unreach-call2.i).

Found 19 witnesses for program sv-benchmarks/c/bitvector-loops/diamond_false-unreach-call2.i, bcf679bfa04b1fbcd635d39b7fcf10b90f13b5b1b9a6cb34d9f932caed50dbe3
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/bcf679bfa04b1fbcd635d39b7fcf10b90f13b5b1b9a6cb34d9f932caed50dbe3.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 35d2bdb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 3 2017-12-01T23:16 CET (sv-comp)
Download d89b24a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 10 Sat Dec 2 19:12:53 2017
Download 160a962 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 13 2017-12-03T04:45Z
Download 217f713 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T12:24 CET (sv-comp)
Download 49d53d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 2 2017-12-01T21:32 CET (sv-comp)
Download 1e8c827 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 13 2017-12-02T17:34Z
Download f918982 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 6 2017-12-01T23:10:12.874919
Download d7ac3e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 6 2017-12-01T09:07:50.859669
Download 824f8e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 6 2017-11-30T16:31 CET (sv-comp)
Download d275647 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 14 2017-12-01T02:27:08+01:00
Download a9892ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 11 2017-11-30T14:47 CET (sv-comp)
Download 7a6e300 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 13 2017-12-02T06:49Z
Download f8574a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 10 2017-11-30T12:17 CET (sv-comp)
Download 20d27cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 10 2017-12-02T15:47:35+01:00 472da85
Download da43efb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 10 2017-12-01T07:41:06+01:00 cfa67e6
Download df9be83 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 10 2017-12-01T07:40:01+01:00 34bfa45
Download 21a6e07 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 22 2017-11-30T21:20:48+01:00
Download a711514 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 10 2017-11-30T14:34:37+01:00
Download 102c1ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 10 2017-12-01T20:40:06+01:00

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

Trying to find witnesses for program (bcf679bfa04b1fbcd635d39b7fcf10b90f13b5b1b9a6cb34d9f932caed50dbe3, sv-benchmarks/c/bitvector-loops/diamond_false-unreach-call2.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector-loops/diamond_false-unreach-call2.i, bcf679bfa04b1fbcd635d39b7fcf10b90f13b5b1b9a6cb34d9f932caed50dbe3
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/bcf679bfa04b1fbcd635d39b7fcf10b90f13b5b1b9a6cb34d9f932caed50dbe3.json

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