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_1_false-no-overflow.i
programSHA 419b9ce5cc38f2044bdd224544108dff800a59778d074a6bded7ddf4ef717838
witnessName results-verified/cpa-seq.2018-12-05_0546.logfiles/sv-comp19_prop-nooverflow.byte_add_1_false-no-overflow.i.files/witness.graphml
witnessSHA 3aa145c9faaeff7bfd5d9c262d0aee4dc647d072d91fe75aef417a5dc5eaf8b0

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-05T05:47:20+01:00
producer CPAchecker 1.7-svn 29852
program-sha256 419b9ce5cc38f2044bdd224544108dff800a59778d074a6bded7ddf4ef717838
programfile ../../sv-benchmarks/c/bitvector/byte_add_1_false-no-overflow.i
programhash 419b9ce5cc38f2044bdd224544108dff800a59778d074a6bded7ddf4ef717838
sourcecodelang C
specification CHECK( init(main()), LTL(G ! overflow) )
witness-file witnessFileByHash/3aa145c9faaeff7bfd5d9c262d0aee4dc647d072d91fe75aef417a5dc5eaf8b0.graphml
witness-sha256 3aa145c9faaeff7bfd5d9c262d0aee4dc647d072d91fe75aef417a5dc5eaf8b0
witness-size 56671
witness-type violation_witness

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

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

Trying to find witnesses for program (419b9ce5cc38f2044bdd224544108dff800a59778d074a6bded7ddf4ef717838, sv-benchmarks/c/bitvector/byte_add_1_false-no-overflow.i).

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c596716 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 25 2019-12-04T01:12 CET (comp)
Download edd6ff8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 56 2019-12-11T21:48:24+01:00 Download 7d2385c
Download c87f9f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 47 2019-12-11T20:55:31+01:00 Download f630658
Download 4ff5770 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 59 2019-12-11T20:44:55+01:00 Download 1642863
Download c001b1e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 57 2019-12-04T02:58:13+01:00 Download c596716
Download 89b5283 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 56 2019-12-03T08:10:36+01:00 Download 81b4f47
Download 81b4f47 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 57 2019-11-30T00:58:04+01:00
Download 7d2385c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 57 2019-11-30T20:43:42+01:00
Download 18b0b18 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 19 2019-12-06T02:42:39+01:00 Download 77c019b
Download 6a997c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 19 2019-12-05T20:20:47+01:00 Download d840c2b
Download c41e543 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 19 2019-12-05T19:35:11+01:00 Download 1c511d4

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

Trying to find witnesses for program (419b9ce5cc38f2044bdd224544108dff800a59778d074a6bded7ddf4ef717838, sv-benchmarks/c/bitvector/byte_add_1_false-no-overflow.i).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a4775aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 1 2018-12-08T05:49 CET (sv-comp)
Download 5595a42 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness SMACK 1.9.3 10 2018-12-08T12:44:11
Download fc227f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 28 2018-12-07T09:46 CET (sv-comp)
Download ff6f364 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 57 2018-12-08T02:55:48+01:00
Download 3b8e1d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 57 2018-12-09T17:47:28+01:00 Download 329f0a7
Download 9480575 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 59 2018-12-08T23:44:04+01:00 Download a4775aa
Download 90e1978 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 47 2018-12-08T22:10:27+01:00 Download 5595a42
Download 55bbc31 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 56 2018-12-08T08:38:33+01:00 Download ff6f364
Download 04d9a82 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 47 2018-12-08T05:02:58+01:00 Download 5d814b9
Download 610fc4d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 59 2018-12-07T17:42:55+01:00 Download fc227f1
Download f25ba72 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 46 2018-12-06T10:19:50+01:00 Download 12e8c2d
Download 3bb26a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 56 2018-12-06T09:48:18+01:00 Download 3aa145c
Download 3aa145c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 57 2018-12-05T05:47:20+01:00
Download e5c4544 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 19 2018-12-06T09:41:43+01:00 Download 16ca8a8
Download 708c21a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 19 2018-12-06T09:19:05+01:00 Download 6d434dd
Download c391305 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 19 2018-12-06T09:05:36+01:00 Download a52335e

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

Trying to find witnesses for program (419b9ce5cc38f2044bdd224544108dff800a59778d074a6bded7ddf4ef717838, sv-benchmarks/c/bitvector/byte_add_1_false-no-overflow.i).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3379238 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 1 2017-12-03T04:23 CET (sv-comp)
Download 5276449 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 4.6.0 kind 8 2017-12-02T18:05:49.438639
Download f0e13b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 4.6.0 incr 8 2017-12-02T05:49:30.405443
Download ce85a1c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 50 2017-12-03T05:20:10+01:00 bbebd3c
Download 5807288 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 43 2017-12-02T20:06:25+01:00 56c77b0
Download fab3845 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 43 2017-12-02T08:14:59+01:00 21e5a32
Download a50a855 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 50 2017-12-01T12:02:03+01:00 27de9c1
Download 9a29620 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 41 2017-12-01T11:19:52+01:00 2149b50
Download 53a50f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 49 2017-12-01T10:55:25+01:00
Download 67c0abc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CBMC 33 2017-12-01T11:30 CET (sv-comp)
Download 0c2cf89 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness 2LS 29 2017-12-01T10:21 CET (sv-comp)
Download 42122e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Map2Check 9 2017-12-02T01:15 CET (sv-comp)
Download b80284e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 3.1 23 2017-12-01T13:49 CET (sv-comp)
Download 7c7d94e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-12-01T12:33:13+01:00 76b9f86

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

Trying to find witnesses for program (419b9ce5cc38f2044bdd224544108dff800a59778d074a6bded7ddf4ef717838, sv-benchmarks/c/bitvector/byte_add_1_false-no-overflow.i).

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

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