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/recursive/Addition03_false-no-overflow.c
programSHA af33174331060e8f80651732b9594cf755d5248b4e0592e6919a829b0dc6a7ca
witnessName results-verified/depthk.2018-12-05_0936.logfiles/sv-comp19_prop-nooverflow.Addition03_false-no-overflow.c.files/witness.graphml
witnessSHA 713b1e51e96f8b5b76b40569ae7828bfc097dffe1e35355c5bad9cb072123be4

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-05T08:41:37.084070
producer DepthK v3.0
programfile /tmp/vcloud-vcloud-master/worker/working_dir_668e0023-e843-4d57-a783-8d2e3f50d654/sv-benchmarks/c/recursive/Addition03_false-no-overflow.c
programhash dddcb69df051b3342ff5d327b07dc16715e4d058
sourcecodelang C
specification CHECK( init(main()), LTL(G ! overflow) )
witness-file witnessFileByHash/713b1e51e96f8b5b76b40569ae7828bfc097dffe1e35355c5bad9cb072123be4.graphml
witness-sha256 713b1e51e96f8b5b76b40569ae7828bfc097dffe1e35355c5bad9cb072123be4
witness-size 4047
witness-type violation_witness

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

Trying to find witnesses for program (af33174331060e8f80651732b9594cf755d5248b4e0592e6919a829b0dc6a7ca, sv-benchmarks/c/recursive/Addition03_false-no-overflow.c).

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

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

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

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

Found 14 witnesses for program sv-benchmarks/c/recursive/Addition03_false-no-overflow.c, af33174331060e8f80651732b9594cf755d5248b4e0592e6919a829b0dc6a7ca
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/af33174331060e8f80651732b9594cf755d5248b4e0592e6919a829b0dc6a7ca.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ecced99 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 1 2019-12-02 00:01:38
Download fee9b06 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 4 2019-12-03T23:58 CET (comp)
Download f675bbb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 6 2019-12-11T21:57:16+01:00 Download 246d8aa
Download af12229 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 6 2019-12-11T21:40:54+01:00 Download 7e9ed21
Download c20f273 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 6 2019-12-11T21:09:32+01:00 Download ecced99
Download f94a5ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 6 2019-12-11T20:44:51+01:00 Download 4f56f38
Download 2cc6e13 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 6 2019-12-08T00:26:17+01:00 Download 56e100a
Download 53eacee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 6 2019-12-07T21:17:27+01:00 Download 0ac789c
Download 3154287 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 14 2019-12-05T20:21:48+01:00 Download 906efdd
Download cf8c077 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 6 2019-12-04T02:58:02+01:00 Download fee9b06
Download 82916e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 6 2019-12-03T08:10:35+01:00 Download 2c90b86
Download 2c90b86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 6 2019-11-29T14:54:03+01:00
Download 7e9ed21 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 6 2019-11-30T21:12:06+01:00
Download dc5fd0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 7 2019-12-11T20:54:52+01:00 Download 935f563

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

Trying to find witnesses for program (af33174331060e8f80651732b9594cf755d5248b4e0592e6919a829b0dc6a7ca, sv-benchmarks/c/recursive/Addition03_false-no-overflow.c).

Found 19 witnesses for program sv-benchmarks/c/recursive/Addition03_false-no-overflow.c, af33174331060e8f80651732b9594cf755d5248b4e0592e6919a829b0dc6a7ca
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/af33174331060e8f80651732b9594cf755d5248b4e0592e6919a829b0dc6a7ca.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 40c10bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 2 2018-12-08T17:51 CET (sv-comp)
Download 9b530f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness SMACK 1.9.3 4 2018-12-08T13:28:05
Download 88f49d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 4 2018-12-07T10:47 CET (sv-comp)
Download 8691d2f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 6 2018-12-07T17:51:20+01:00
Download 2ba9920 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-09T20:53:06+01:00 Download 87fa4a1
Download a765561 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-09T20:35:11+01:00 Download 5d864bb
Download 5062cb0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-09T20:22:09+01:00 Download ac80578
Download ad39d6a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-09T18:21:34+01:00 Download d01ac4c
Download b6a45fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T23:44:33+01:00 Download 40c10bf
Download 2460aaa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T22:10:12+01:00 Download 9b530f2
Download 700492c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T09:00:37+01:00 Download 8691d2f
Download 975b1c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T05:03:54+01:00 Download e5c8086
Download 82c6fd8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-07T17:43:34+01:00 Download 88f49d0
Download ea9e955 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-07T01:07:13+01:00 Download d64a226
Download b580a09 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T10:19:56+01:00 Download 713b1e5
Download b1d0a25 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:48:17+01:00 Download c943fe9
Download f760cb3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 18 2018-12-06T09:14:37+01:00 Download d3a8bb1
Download 1ea2665 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:00:54+01:00 Download 7212ff4
Download c943fe9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T01:48:33+01:00

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

Trying to find witnesses for program (af33174331060e8f80651732b9594cf755d5248b4e0592e6919a829b0dc6a7ca, sv-benchmarks/c/recursive/Addition03_false-no-overflow.c).

Found 20 witnesses for program sv-benchmarks/c/recursive/Addition03_false-no-overflow.c, af33174331060e8f80651732b9594cf755d5248b4e0592e6919a829b0dc6a7ca
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/af33174331060e8f80651732b9594cf755d5248b4e0592e6919a829b0dc6a7ca.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 4f6e8e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Taipan 5 2017-12-03T07:43Z
Download 1b4af0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 2 2017-12-03T04:20 CET (sv-comp)
Download cf9b340 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Map2Check 3 2017-12-02T01:33 CET (sv-comp)
Download 20fdcd0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Kojak 5 2017-12-03T10:24Z
Download 8db3cc4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T18:23:53.760328
Download f0dc1dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-02T06:42:29.384810
Download b1e68f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 3.1 4 2017-12-01T14:06 CET (sv-comp)
Download a0b9d0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T11:53:00+01:00 7f8a5dd
Download 9d7fd2f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T11:52:09+01:00 5456e3d
Download e21dd60 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T08:58:56+01:00 a38313b
Download d9ab60d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 6 2017-12-03T05:13:39+01:00 62d2b8c
Download b3d48a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T20:08:42+01:00 70958ff
Download 15bc545 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T08:11:27+01:00 669ccc4
Download 9aca4ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T02:13:24+01:00 a1b92c8
Download a3db3a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 17 2017-12-01T12:33:22+01:00 bff078e
Download 426b709 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T12:02:01+01:00 7a1bce9
Download 856565d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T10:53:41+01:00
Download 2453ad0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CBMC 8 2017-12-01T11:20 CET (sv-comp)
Download a31d170 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Automizer 5 2017-12-03T10:34Z
Download e7246ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T14:47:32+01:00 b2a929f

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

Trying to find witnesses for program (af33174331060e8f80651732b9594cf755d5248b4e0592e6919a829b0dc6a7ca, sv-benchmarks/c/recursive/Addition03_false-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/recursive/Addition03_false-no-overflow.c, af33174331060e8f80651732b9594cf755d5248b4e0592e6919a829b0dc6a7ca
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/af33174331060e8f80651732b9594cf755d5248b4e0592e6919a829b0dc6a7ca.json

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