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/reducercommutativity/rangesum20_false-unreach-call.i
programSHA ba03910c4491171ab76870ab4758329e93bd5a9463481cc53366002d0ed13f15
witnessName results-verified/pinaka.2018-12-06_2014.logfiles/sv-comp19_prop-reachsafety.rangesum20_false-unreach-call.i.files/witness.graphml
witnessSHA cdd685f5789c28c447e0c1e4173e85396dff9562b0c816f4b3df0ea7f54f61c2

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-07T05:16 CET (sv-comp)
producer Pinaka
program-sha256 ba03910c4491171ab76870ab4758329e93bd5a9463481cc53366002d0ed13f15
programfile ../../sv-benchmarks/c/reducercommutativity/rangesum20_false-unreach-call.i
programhash ba03910c4491171ab76870ab4758329e93bd5a9463481cc53366002d0ed13f15
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/cdd685f5789c28c447e0c1e4173e85396dff9562b0c816f4b3df0ea7f54f61c2.graphml
witness-sha256 cdd685f5789c28c447e0c1e4173e85396dff9562b0c816f4b3df0ea7f54f61c2
witness-size 87798
witness-type violation_witness

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

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

Trying to find witnesses for program (ba03910c4491171ab76870ab4758329e93bd5a9463481cc53366002d0ed13f15, sv-benchmarks/c/reducercommutativity/rangesum20_false-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/reducercommutativity/rangesum20_false-unreach-call.i, ba03910c4491171ab76870ab4758329e93bd5a9463481cc53366002d0ed13f15
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/ba03910c4491171ab76870ab4758329e93bd5a9463481cc53366002d0ed13f15.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 (ba03910c4491171ab76870ab4758329e93bd5a9463481cc53366002d0ed13f15, sv-benchmarks/c/reducercommutativity/rangesum20_false-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/reducercommutativity/rangesum20_false-unreach-call.i, ba03910c4491171ab76870ab4758329e93bd5a9463481cc53366002d0ed13f15
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/ba03910c4491171ab76870ab4758329e93bd5a9463481cc53366002d0ed13f15.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 (ba03910c4491171ab76870ab4758329e93bd5a9463481cc53366002d0ed13f15, sv-benchmarks/c/reducercommutativity/rangesum20_false-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/reducercommutativity/rangesum20_false-unreach-call.i, ba03910c4491171ab76870ab4758329e93bd5a9463481cc53366002d0ed13f15
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/ba03910c4491171ab76870ab4758329e93bd5a9463481cc53366002d0ed13f15.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 (ba03910c4491171ab76870ab4758329e93bd5a9463481cc53366002d0ed13f15, sv-benchmarks/c/reducercommutativity/rangesum20_false-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/reducercommutativity/rangesum20_false-unreach-call.i, ba03910c4491171ab76870ab4758329e93bd5a9463481cc53366002d0ed13f15
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/ba03910c4491171ab76870ab4758329e93bd5a9463481cc53366002d0ed13f15.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 (ba03910c4491171ab76870ab4758329e93bd5a9463481cc53366002d0ed13f15, sv-benchmarks/c/reducercommutativity/rangesum20_false-unreach-call.i).

Found 15 witnesses for program sv-benchmarks/c/reducercommutativity/rangesum20_false-unreach-call.i, ba03910c4491171ab76870ab4758329e93bd5a9463481cc53366002d0ed13f15
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/ba03910c4491171ab76870ab4758329e93bd5a9463481cc53366002d0ed13f15.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 473023d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 5 2019-12-01 14:18:08
Download e3ee562 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 82 2019-12-04T01:01 CET (comp)
Download da4691e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 172 2019-12-11T21:49:38+01:00 Download 69f8417
Download 1a77d8a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 172 2019-12-11T21:09:54+01:00 Download 473023d
Download 90f4a09 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 172 2019-12-11T20:45:12+01:00 Download 5c5121b
Download 69f8417 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 166 2019-12-01T00:11:59+01:00
Download e527703 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 11 2019-12-11T20:54:50+01:00 Download 1209165
Download 35ab292 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 12 2019-12-08T01:51:16+01:00 Download 0a27a6d
Download 8605ff2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 12 2019-12-08T00:26:24+01:00 Download 1a6a4de
Download be82032 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 12 2019-12-06T02:38:46+01:00 Download fd6d8ed
Download b5cc623 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 10 2019-12-05T20:20:41+01:00 Download c14a176
Download 8827999 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 12 2019-12-04T02:58:07+01:00 Download e3ee562
Download 00cf0a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 12 2019-12-03T08:58:24+01:00 Download 2f3bb14
Download 72fd70b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 10 2019-12-03T08:10:25+01:00 Download 73ca3cb
Download 73ca3cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 15 2019-11-30T02:23:53+01:00

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

Trying to find witnesses for program (ba03910c4491171ab76870ab4758329e93bd5a9463481cc53366002d0ed13f15, sv-benchmarks/c/reducercommutativity/rangesum20_false-unreach-call.i).

Found 20 witnesses for program sv-benchmarks/c/reducercommutativity/rangesum20_false-unreach-call.i, ba03910c4491171ab76870ab4758329e93bd5a9463481cc53366002d0ed13f15
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/ba03910c4491171ab76870ab4758329e93bd5a9463481cc53366002d0ed13f15.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 53cafd8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T08:09 CET (sv-comp)
Download f52c1c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T03:52:03
Download cdd685f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 88 2018-12-07T05:16 CET (sv-comp)
Download c0c53e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 152 2018-12-10T17:56:22+01:00
Download 3b78823 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 166 2018-12-07T19:37:15+01:00
Download ef4dfaa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 172 2018-12-09T18:19:55+01:00 Download b08b0f1
Download b0531ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 172 2018-12-08T22:10:22+01:00 Download f52c1c5
Download 93ee44d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 172 2018-12-08T08:47:46+01:00 Download 3b78823
Download 5661e0e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 172 2018-12-07T18:47:24+01:00 Download 1d4ab85
Download b8d7117 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-10T20:35:20+01:00 Download c0c53e0
Download eb3ebf0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-09T20:24:00+01:00 Download dcb33e4
Download b48a78b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-08T23:44:12+01:00 Download 53cafd8
Download 64fea04 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-08T04:57:02+01:00 Download a1d9299
Download 6f77eca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-08T03:37:51+01:00 Download 4c9701d
Download 2030a52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-07T17:45:18+01:00 Download cdd685f
Download 53d5fdb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-06T10:17:23+01:00 Download 4054573
Download 99c1d4b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-06T09:50:33+01:00 Download 02c4a91
Download 8d36e41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-06T09:18:11+01:00 Download 25705de
Download becde94 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-06T09:09:19+01:00 Download 01fb13a
Download 02c4a91 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 15 2018-12-05T16:28:52+01:00

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

Trying to find witnesses for program (ba03910c4491171ab76870ab4758329e93bd5a9463481cc53366002d0ed13f15, sv-benchmarks/c/reducercommutativity/rangesum20_false-unreach-call.i).

Found 13 witnesses for program sv-benchmarks/c/reducercommutativity/rangesum20_false-unreach-call.i, ba03910c4491171ab76870ab4758329e93bd5a9463481cc53366002d0ed13f15
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/ba03910c4491171ab76870ab4758329e93bd5a9463481cc53366002d0ed13f15.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5c886b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 3 2017-12-01T22:58 CET (sv-comp)
Download 1271f86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VIAP 4 2017-12-03T03:56 CET (sv-comp)
Download d05172e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T11:00 CET (sv-comp)
Download ca004e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 7 2017-12-01T20:05 CET (sv-comp)
Download 02b6389 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 109 2017-12-02T07:42Z
Download f516ac4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 19 2017-12-02T00:29:34.815569
Download 8890128 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 19 2017-12-01T07:49:57.295397
Download 3c230b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 39 2017-11-30T20:04 CET (sv-comp)
Download 56f5a26 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 148 2017-12-02T22:50:20+01:00
Download 065cae7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 189 2017-11-30T16:21:56+01:00
Download 24d1a2c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 114 2017-11-30T13:19:36+01:00
Download 67e8dd4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 88 2017-12-02T00:20:20+01:00
Download b7d758b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 94 2017-11-30T20:34 CET (sv-comp)

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

Trying to find witnesses for program (ba03910c4491171ab76870ab4758329e93bd5a9463481cc53366002d0ed13f15, sv-benchmarks/c/reducercommutativity/rangesum20_false-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/reducercommutativity/rangesum20_false-unreach-call.i, ba03910c4491171ab76870ab4758329e93bd5a9463481cc53366002d0ed13f15
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/ba03910c4491171ab76870ab4758329e93bd5a9463481cc53366002d0ed13f15.json

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