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/byte_add_false-no-overflow.i
programSHA 99425cd66d2a59d5d5f6ed66b3daa7f9de2fff0d25311bf1b228e17ef45fe4f4
witnessName results-validated/cpa-seq-validate-violation-witnesses-pesco.2018-12-08_0739.logfiles/sv-comp19_prop-nooverflow.byte_add_false-no-overflow.i.files/witness.graphml
witnessSHA 8bba968d084450cd1f98f2075a14ffaa5d247bf43c287f497e7076566ffa3df9

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-08T08:13:35+01:00
inputwitnesshash 45f57ac4da9fb78f5ef30765119dcc06c040befa1965541dc0714217a91c8dbd
producer CPAchecker 1.7-svn 29852
program-sha256 99425cd66d2a59d5d5f6ed66b3daa7f9de2fff0d25311bf1b228e17ef45fe4f4
programfile ../../sv-benchmarks/c/bitvector/byte_add_false-no-overflow.i
programhash 99425cd66d2a59d5d5f6ed66b3daa7f9de2fff0d25311bf1b228e17ef45fe4f4
sourcecodelang C
specification CHECK( init(main()), LTL(G ! overflow) )
witness-file witnessFileByHash/8bba968d084450cd1f98f2075a14ffaa5d247bf43c287f497e7076566ffa3df9.graphml
witness-sha256 8bba968d084450cd1f98f2075a14ffaa5d247bf43c287f497e7076566ffa3df9
witness-size 51912
witness-type violation_witness

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

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

Trying to find witnesses for program (99425cd66d2a59d5d5f6ed66b3daa7f9de2fff0d25311bf1b228e17ef45fe4f4, sv-benchmarks/c/bitvector/byte_add_false-no-overflow.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector/byte_add_false-no-overflow.i, 99425cd66d2a59d5d5f6ed66b3daa7f9de2fff0d25311bf1b228e17ef45fe4f4
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/99425cd66d2a59d5d5f6ed66b3daa7f9de2fff0d25311bf1b228e17ef45fe4f4.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 (99425cd66d2a59d5d5f6ed66b3daa7f9de2fff0d25311bf1b228e17ef45fe4f4, sv-benchmarks/c/bitvector/byte_add_false-no-overflow.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector/byte_add_false-no-overflow.i, 99425cd66d2a59d5d5f6ed66b3daa7f9de2fff0d25311bf1b228e17ef45fe4f4
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/99425cd66d2a59d5d5f6ed66b3daa7f9de2fff0d25311bf1b228e17ef45fe4f4.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 (99425cd66d2a59d5d5f6ed66b3daa7f9de2fff0d25311bf1b228e17ef45fe4f4, sv-benchmarks/c/bitvector/byte_add_false-no-overflow.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector/byte_add_false-no-overflow.i, 99425cd66d2a59d5d5f6ed66b3daa7f9de2fff0d25311bf1b228e17ef45fe4f4
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/99425cd66d2a59d5d5f6ed66b3daa7f9de2fff0d25311bf1b228e17ef45fe4f4.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 (99425cd66d2a59d5d5f6ed66b3daa7f9de2fff0d25311bf1b228e17ef45fe4f4, sv-benchmarks/c/bitvector/byte_add_false-no-overflow.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector/byte_add_false-no-overflow.i, 99425cd66d2a59d5d5f6ed66b3daa7f9de2fff0d25311bf1b228e17ef45fe4f4
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/99425cd66d2a59d5d5f6ed66b3daa7f9de2fff0d25311bf1b228e17ef45fe4f4.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 (99425cd66d2a59d5d5f6ed66b3daa7f9de2fff0d25311bf1b228e17ef45fe4f4, sv-benchmarks/c/bitvector/byte_add_false-no-overflow.i).

Found 11 witnesses for program sv-benchmarks/c/bitvector/byte_add_false-no-overflow.i, 99425cd66d2a59d5d5f6ed66b3daa7f9de2fff0d25311bf1b228e17ef45fe4f4
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/99425cd66d2a59d5d5f6ed66b3daa7f9de2fff0d25311bf1b228e17ef45fe4f4.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6e001ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 24 2019-12-03T22:37 CET (comp)
Download e599921 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 53 2019-12-11T21:43:05+01:00 Download 3a547da
Download 6376255 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 47 2019-12-11T20:55:12+01:00 Download 2491f4c
Download 21f7a36 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 53 2019-12-11T20:44:29+01:00 Download 9abb9e3
Download edc46b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 57 2019-12-04T02:58:12+01:00 Download 6e001ff
Download 9d0c1f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 53 2019-12-03T08:10:35+01:00 Download 9febdc9
Download 9febdc9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 53 2019-11-30T11:38:28+01:00
Download 3a547da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 53 2019-12-01T14:50:31+01:00
Download 31cc05d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 19 2019-12-06T02:39:01+01:00 Download 73fbf04
Download 5afc613 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 19 2019-12-05T20:20:13+01:00 Download 8702607
Download 618743b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 19 2019-12-05T19:34:22+01:00 Download 4f2de2b

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

Trying to find witnesses for program (99425cd66d2a59d5d5f6ed66b3daa7f9de2fff0d25311bf1b228e17ef45fe4f4, sv-benchmarks/c/bitvector/byte_add_false-no-overflow.i).

Found 16 witnesses for program sv-benchmarks/c/bitvector/byte_add_false-no-overflow.i, 99425cd66d2a59d5d5f6ed66b3daa7f9de2fff0d25311bf1b228e17ef45fe4f4
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/99425cd66d2a59d5d5f6ed66b3daa7f9de2fff0d25311bf1b228e17ef45fe4f4.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download dcc9e8e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 2 2018-12-08T13:25 CET (sv-comp)
Download 3a30046 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness SMACK 1.9.3 10 2018-12-08T02:53:28
Download de09cc6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 30 2018-12-06T23:54 CET (sv-comp)
Download 45f57ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 52 2018-12-08T00:13:20+01:00
Download ea00e93 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 63 2018-12-09T18:21:00+01:00 Download b0e2c84
Download 380cfd1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 57 2018-12-08T23:44:49+01:00 Download dcc9e8e
Download 39ac3fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 47 2018-12-08T22:10:56+01:00 Download 3a30046
Download 8bba968 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 52 2018-12-08T08:13:35+01:00 Download 45f57ac
Download d851595 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 47 2018-12-08T05:04:40+01:00 Download d1a634a
Download 4c90825 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 60 2018-12-07T17:44:10+01:00 Download de09cc6
Download 781c7a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 56 2018-12-06T10:10:10+01:00 Download f6f0798
Download 3a3b59e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 52 2018-12-06T09:48:50+01:00 Download 0c2e311
Download 0c2e311 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 52 2018-12-06T04:29:57+01:00
Download 456d502 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 19 2018-12-06T09:40:49+01:00 Download 7a382d6
Download 5fcc330 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 19 2018-12-06T09:20:02+01:00 Download a5c809b
Download f167cda Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 19 2018-12-06T09:15:39+01:00 Download 38ef01e

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

Trying to find witnesses for program (99425cd66d2a59d5d5f6ed66b3daa7f9de2fff0d25311bf1b228e17ef45fe4f4, sv-benchmarks/c/bitvector/byte_add_false-no-overflow.i).

Found 14 witnesses for program sv-benchmarks/c/bitvector/byte_add_false-no-overflow.i, 99425cd66d2a59d5d5f6ed66b3daa7f9de2fff0d25311bf1b228e17ef45fe4f4
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/99425cd66d2a59d5d5f6ed66b3daa7f9de2fff0d25311bf1b228e17ef45fe4f4.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 19213b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 2 2017-12-03T04:19 CET (sv-comp)
Download 34ac8dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 4.6.0 kind 9 2017-12-02T17:36:12.163715
Download eaf8148 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 4.6.0 incr 9 2017-12-02T05:33:58.405164
Download 3118705 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 49 2017-12-03T05:14:57+01:00 c50e4d3
Download e4064d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 43 2017-12-02T20:08:54+01:00 09269a8
Download dad9836 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 43 2017-12-02T08:11:47+01:00 74b7216
Download bbd2e16 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 46 2017-12-01T12:02:13+01:00 6f7e820
Download c92b2b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 41 2017-12-01T11:19:24+01:00 3513196
Download 8794dba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 46 2017-12-01T11:03:26+01:00
Download 0064980 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CBMC 35 2017-12-01T12:00 CET (sv-comp)
Download f7a279e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness 2LS 29 2017-12-01T10:43 CET (sv-comp)
Download 0609d3c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Map2Check 11 2017-12-02T01:21 CET (sv-comp)
Download 1f5f403 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 3.1 24 2017-12-01T13:53 CET (sv-comp)
Download 9514bb7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-12-01T12:32:59+01:00 f48c9cb

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

Trying to find witnesses for program (99425cd66d2a59d5d5f6ed66b3daa7f9de2fff0d25311bf1b228e17ef45fe4f4, sv-benchmarks/c/bitvector/byte_add_false-no-overflow.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector/byte_add_false-no-overflow.i, 99425cd66d2a59d5d5f6ed66b3daa7f9de2fff0d25311bf1b228e17ef45fe4f4
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/99425cd66d2a59d5d5f6ed66b3daa7f9de2fff0d25311bf1b228e17ef45fe4f4.json

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