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-simple/sum_non_eq_false-no-overflow.c
programSHA 40c927fbd2f6ec96aba981d248406fa89326af0e54ef63b3f247d52021471902
witnessName results-verified/esbmc-incr.2017-12-02_0623.logfiles/sv-comp18.sum_non_eq_false-no-overflow.c.files/witness.graphml
witnessSHA c73684855b60224bda3a47ee7afbad4b15c616b16b2dbb2f42f39b7fe7ccb8ec

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/c73684855b60224bda3a47ee7afbad4b15c616b16b2dbb2f42f39b7fe7ccb8ec.json

Key Value
architecture 32bit
creationtime 2017-12-02T05:29:17.400193
producer ESBMC 4.6.0 incr
program-sha256 40c927fbd2f6ec96aba981d248406fa89326af0e54ef63b3f247d52021471902
programfile ../../sv-benchmarks/c/recursive-simple/sum_non_eq_false-no-overflow.c
programhash c3f4ddad1399519940e721d52a976bc45ffd3619
sourcecodelang C
specification CHECK( init(main()), LTL(G ! overflow) )
witness-file witnessFileByHash/c73684855b60224bda3a47ee7afbad4b15c616b16b2dbb2f42f39b7fe7ccb8ec.graphml
witness-sha256 c73684855b60224bda3a47ee7afbad4b15c616b16b2dbb2f42f39b7fe7ccb8ec
witness-size 3985
witness-type violation_witness

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

Trying to find witnesses for program (40c927fbd2f6ec96aba981d248406fa89326af0e54ef63b3f247d52021471902, sv-benchmarks/c/recursive-simple/sum_non_eq_false-no-overflow.c).

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 21a4aef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 1 2019-12-01 15:22:15
Download df85606 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 4 2019-12-03T22:21 CET (comp)
Download 3978234 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-11T21:44:43+01:00 Download cbc271f
Download e999847 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-11T21:40:43+01:00 Download 31f91c5
Download b257878 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-11T21:09:00+01:00 Download 21a4aef
Download 9ed1f6b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-11T20:44:25+01:00 Download 78b57d1
Download cdf1cda Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-08T00:26:13+01:00 Download 6fc5814
Download f9976bb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-07T21:16:00+01:00 Download 16f30e3
Download 3174d1c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-05T20:21:29+01:00 Download 65ffb61
Download feae320 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-04T02:58:02+01:00 Download df85606
Download edce4f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-03T08:09:52+01:00 Download 5a16f44
Download 5a16f44 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-11-29T23:44:59+01:00
Download cbc271f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 5 2019-12-01T12:22:00+01:00
Download bf7af07 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 5 2019-12-11T20:54:56+01:00 Download f762b29

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

Trying to find witnesses for program (40c927fbd2f6ec96aba981d248406fa89326af0e54ef63b3f247d52021471902, sv-benchmarks/c/recursive-simple/sum_non_eq_false-no-overflow.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download cde8083 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 2 2018-12-08T07:25 CET (sv-comp)
Download 9b37006 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness SMACK 1.9.3 4 2018-12-08T07:09:36
Download cb71f82 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 4 2018-12-07T11:00 CET (sv-comp)
Download 5682d9b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-07T10:45:48+01:00
Download 4dfc23c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:53:05+01:00 Download 46babc6
Download 6423ecd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:39:41+01:00 Download a7ac9b0
Download ff7f74a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:32:51+01:00 Download 9437d5a
Download 57305e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T18:21:18+01:00 Download 6a016e0
Download 23689dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T23:44:52+01:00 Download cde8083
Download bfc5988 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T22:08:48+01:00 Download 9b37006
Download 6de9da6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T08:03:22+01:00 Download 5682d9b
Download 6f0e015 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T04:56:34+01:00 Download 693225d
Download ef97a9e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-07T17:43:51+01:00 Download cb71f82
Download 7fef990 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-07T01:06:24+01:00 Download a7b8560
Download 6fea9d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T10:17:39+01:00 Download 46893d5
Download 93c8942 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:47:56+01:00 Download 5a3295a
Download 11e9b41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:16:32+01:00 Download c8ac7ba
Download 1dc1196 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:10:22+01:00 Download 391e0c3
Download 5a3295a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T01:03:26+01:00

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

Trying to find witnesses for program (40c927fbd2f6ec96aba981d248406fa89326af0e54ef63b3f247d52021471902, sv-benchmarks/c/recursive-simple/sum_non_eq_false-no-overflow.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 1f98ef0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Taipan 4 2017-12-03T07:44Z
Download 28f9825 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 2 2017-12-03T04:10 CET (sv-comp)
Download 0f343e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Map2Check 3 2017-12-02T01:14 CET (sv-comp)
Download 1659075 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Kojak 4 2017-12-03T10:33Z
Download 6d00846 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T18:23:47.396534
Download c736848 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-02T05:29:17.400193
Download 1aa97a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 3.1 5 2017-12-01T14:16 CET (sv-comp)
Download 32e3209 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T11:52:57+01:00 082b339
Download b6ecbd4 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 ab8c3ca
Download 514ceaf 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 14326f0
Download 81c3f6c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T05:18:15+01:00 7838ded
Download 80cfcd5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T20:07:53+01:00 332a027
Download e2e1d06 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T08:10:54+01:00 4115b87
Download c10547f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T02:13:18+01:00 a3faede
Download f16b25a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T12:33:21+01:00 8c96333
Download 6e0b5b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T12:02:05+01:00 5aa607b
Download 5dbbe55 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T11:45:25+01:00
Download 7cf42f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CBMC 6 2017-12-01T12:06 CET (sv-comp)
Download c286db8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Automizer 4 2017-12-03T10:21Z
Download 55804d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T14:46:56+01:00 23dec9c

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

Trying to find witnesses for program (40c927fbd2f6ec96aba981d248406fa89326af0e54ef63b3f247d52021471902, sv-benchmarks/c/recursive-simple/sum_non_eq_false-no-overflow.c).

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

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