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/diamond_false-unreach-call1.i
programSHA 2625d4aa05591d1f103074ce250af10eb32a5d248515eb0bb4a1272d1db8df40
witnessName results-verified/verifuzz.2018-12-09_0247.logfiles/sv-comp19_prop-reachsafety.diamond_false-unreach-call1.i.files/witness.graphml
witnessSHA a112715d0d8444601f2447f37b0664bd130784b2d7195270ff3ceff3462bf776

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-09T17:04 CET (sv-comp)
memorymodel precise
producer verifuzz
programfile /home/benchexec/VERIFUZZ_TEMP_DIR/OUT/diamond_false-unreach-call1.i
programhash 584541137f24f4112db8a804424c91b4b8c89eec
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/a112715d0d8444601f2447f37b0664bd130784b2d7195270ff3ceff3462bf776.graphml
witness-sha256 a112715d0d8444601f2447f37b0664bd130784b2d7195270ff3ceff3462bf776
witness-size 2239
witness-type violation_witness

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

Trying to find witnesses for program (2625d4aa05591d1f103074ce250af10eb32a5d248515eb0bb4a1272d1db8df40, sv-benchmarks/c/loop-acceleration/diamond_false-unreach-call1.i).

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

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

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

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

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

Found 20 witnesses for program sv-benchmarks/c/loop-acceleration/diamond_false-unreach-call1.i, 2625d4aa05591d1f103074ce250af10eb32a5d248515eb0bb4a1272d1db8df40
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/2625d4aa05591d1f103074ce250af10eb32a5d248515eb0bb4a1272d1db8df40.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 4ce2c53 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T05:59 CET (sv-comp)
Download 451e23d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 15 2018-12-08T14:21:50
Download a7dcdfe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 79 2018-12-07T09:13 CET (sv-comp)
Download 2ac0904 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 72 2018-12-10T17:44:29+01:00
Download 7b5556b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 76 2018-12-07T01:14:52+01:00
Download c5ed383 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 76 2018-12-10T20:34:56+01:00 Download 2ac0904
Download 8d31404 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 77 2018-12-09T21:24:06+01:00 Download ea2ab64
Download 8f98df5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 77 2018-12-09T18:22:09+01:00 Download a112715
Download 68691d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 145 2018-12-08T23:44:32+01:00 Download 4ce2c53
Download 9db791f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 76 2018-12-08T22:09:34+01:00 Download 451e23d
Download a173379 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 76 2018-12-08T08:20:05+01:00 Download 7b5556b
Download 7308f23 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 77 2018-12-08T03:30:21+01:00 Download 67b189a
Download ba7d074 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 145 2018-12-07T17:44:16+01:00 Download a7dcdfe
Download 6d2aab1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 76 2018-12-06T09:47:54+01:00 Download 9616f1b
Download 4c70e85 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 76 2018-12-06T09:18:10+01:00 Download 04f2782
Download 9616f1b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 77 2018-12-05T11:08:42+01:00
Download 68e0fd1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T05:03:21+01:00 Download 82b7bd4
Download c569721 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-07T01:18:18+01:00 Download f03383e
Download 7296857 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T10:15:17+01:00 Download 13aacc4
Download e157f11 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:42:07+01:00 Download 4aaea91

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

Trying to find witnesses for program (2625d4aa05591d1f103074ce250af10eb32a5d248515eb0bb4a1272d1db8df40, sv-benchmarks/c/loop-acceleration/diamond_false-unreach-call1.i).

Found 13 witnesses for program sv-benchmarks/c/loop-acceleration/diamond_false-unreach-call1.i, 2625d4aa05591d1f103074ce250af10eb32a5d248515eb0bb4a1272d1db8df40
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/2625d4aa05591d1f103074ce250af10eb32a5d248515eb0bb4a1272d1db8df40.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 45443c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VIAP 55 2017-12-03T03:54 CET (sv-comp)
Download 2ec385f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T15:23 CET (sv-comp)
Download 6ffaf12 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 2 2017-12-01T20:19 CET (sv-comp)
Download 84a67dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 13 2017-12-01T23:50:27.804822
Download 88e9451 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 13 2017-12-01T11:44:18.945031
Download 4e82446 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 14 2017-11-30T19:12 CET (sv-comp)
Download cafddbe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 67 2017-12-03T01:40:19+01:00
Download 718d711 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 72 2017-12-01T02:07:20+01:00
Download 0f6222b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 77 2017-12-01T01:16:55+01:00
Download 879aeff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 67 2017-12-01T00:56:00+01:00
Download 726e549 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 56 2017-12-02T11:09:56+01:00
Download c9a72c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 47 2017-11-30T23:08 CET (sv-comp)
Download fb57d73 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 47 2017-11-30T19:29 CET (sv-comp)

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

Trying to find witnesses for program (2625d4aa05591d1f103074ce250af10eb32a5d248515eb0bb4a1272d1db8df40, sv-benchmarks/c/loop-acceleration/diamond_false-unreach-call1.i).

Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/diamond_false-unreach-call1.i, 2625d4aa05591d1f103074ce250af10eb32a5d248515eb0bb4a1272d1db8df40
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/2625d4aa05591d1f103074ce250af10eb32a5d248515eb0bb4a1272d1db8df40.json

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