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_15x0_false-unreach-call_true-termination.c
programSHA 5c29a2f2e6fd473ca90321383d237316a972788e34fdd534748a8440dc3d2534
witnessName results-verified/skink.2018-12-07_1200.logfiles/sv-comp19_prop-reachsafety.sum_15x0_false-unreach-call_true-termination.c.files/witness.graphml
witnessSHA a51daf15cf339b7beb35a17291a9e925e0b54083f34c62a8341dccc89a6976f8

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-07T15:15 CET (sv-comp)
memorymodel simple
producer skink
programfile ../../sv-benchmarks/c/recursive-simple/sum_15x0_false-unreach-call_true-termination.c
programhash 31319b3dce926b7eddaa50d24c240f6870931f21
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/a51daf15cf339b7beb35a17291a9e925e0b54083f34c62a8341dccc89a6976f8.graphml
witness-sha256 a51daf15cf339b7beb35a17291a9e925e0b54083f34c62a8341dccc89a6976f8
witness-size 2496
witness-type violation_witness

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

Trying to find witnesses for program (5c29a2f2e6fd473ca90321383d237316a972788e34fdd534748a8440dc3d2534, sv-benchmarks/c/recursive-simple/sum_15x0_false-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/sum_15x0_false-unreach-call_true-termination.c, 5c29a2f2e6fd473ca90321383d237316a972788e34fdd534748a8440dc3d2534
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/5c29a2f2e6fd473ca90321383d237316a972788e34fdd534748a8440dc3d2534.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 (5c29a2f2e6fd473ca90321383d237316a972788e34fdd534748a8440dc3d2534, sv-benchmarks/c/recursive-simple/sum_15x0_false-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/sum_15x0_false-unreach-call_true-termination.c, 5c29a2f2e6fd473ca90321383d237316a972788e34fdd534748a8440dc3d2534
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/5c29a2f2e6fd473ca90321383d237316a972788e34fdd534748a8440dc3d2534.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 (5c29a2f2e6fd473ca90321383d237316a972788e34fdd534748a8440dc3d2534, sv-benchmarks/c/recursive-simple/sum_15x0_false-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/sum_15x0_false-unreach-call_true-termination.c, 5c29a2f2e6fd473ca90321383d237316a972788e34fdd534748a8440dc3d2534
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/5c29a2f2e6fd473ca90321383d237316a972788e34fdd534748a8440dc3d2534.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 (5c29a2f2e6fd473ca90321383d237316a972788e34fdd534748a8440dc3d2534, sv-benchmarks/c/recursive-simple/sum_15x0_false-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/sum_15x0_false-unreach-call_true-termination.c, 5c29a2f2e6fd473ca90321383d237316a972788e34fdd534748a8440dc3d2534
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/5c29a2f2e6fd473ca90321383d237316a972788e34fdd534748a8440dc3d2534.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 (5c29a2f2e6fd473ca90321383d237316a972788e34fdd534748a8440dc3d2534, sv-benchmarks/c/recursive-simple/sum_15x0_false-unreach-call_true-termination.c).

Found 18 witnesses for program sv-benchmarks/c/recursive-simple/sum_15x0_false-unreach-call_true-termination.c, 5c29a2f2e6fd473ca90321383d237316a972788e34fdd534748a8440dc3d2534
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/5c29a2f2e6fd473ca90321383d237316a972788e34fdd534748a8440dc3d2534.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 80d4f0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 05:28:45
Download 67df420 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 11 2019-12-04T01:20 CET (comp)
Download c0e79ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 22 2019-12-11T21:58:14+01:00 Download 8d1ee38
Download 305593d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 22 2019-12-11T21:42:06+01:00 Download 9865041
Download c7dc642 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 22 2019-12-11T21:09:25+01:00 Download 80d4f0f
Download e543411 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 22 2019-12-11T20:54:21+01:00 Download 061d39f
Download f8e4bad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 22 2019-12-11T20:44:43+01:00 Download bf0547e
Download 7db9ece Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 22 2019-12-08T00:26:04+01:00 Download e72253b
Download 71b9a14 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 22 2019-12-07T21:13:09+01:00 Download 70d5fe6
Download f4ae47d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 22 2019-12-06T02:40:44+01:00 Download 5eef5e6
Download cf46595 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 22 2019-12-04T02:58:26+01:00 Download 67df420
Download f6e0734 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 22 2019-12-03T08:56:47+01:00 Download 96daa0f
Download 663bd56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 22 2019-12-03T08:08:05+01:00 Download 4c29978
Download 4c29978 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 22 2019-11-29T20:34:25+01:00
Download 8d1ee38 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 22 2019-12-01T10:28:56+01:00
Download 37fac93 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-08T01:51:22+01:00 Download a6dd23e
Download 317a4a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-05T20:20:45+01:00 Download c62217a
Download 9edec4a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T23:48 CET (comp)

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

Trying to find witnesses for program (5c29a2f2e6fd473ca90321383d237316a972788e34fdd534748a8440dc3d2534, sv-benchmarks/c/recursive-simple/sum_15x0_false-unreach-call_true-termination.c).

Found 26 witnesses for program sv-benchmarks/c/recursive-simple/sum_15x0_false-unreach-call_true-termination.c, 5c29a2f2e6fd473ca90321383d237316a972788e34fdd534748a8440dc3d2534
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/5c29a2f2e6fd473ca90321383d237316a972788e34fdd534748a8440dc3d2534.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8daa4d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T04:03 CET (sv-comp)
Download 8e13c08 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T01:21:02
Download 28f66ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 12 2018-12-07T07:04 CET (sv-comp)
Download 2543ffc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 22 2018-12-08T04:27:40+01:00
Download 6fb7696 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 22 2018-12-10T10:48:51+01:00 Download 0b9bd27
Download 0d1a25c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 22 2018-12-09T21:23:34+01:00 Download 1497f43
Download 4349943 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 22 2018-12-09T20:53:18+01:00 Download d57544c
Download 34c4476 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 22 2018-12-09T20:39:08+01:00 Download 0065d63
Download 27991d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 22 2018-12-09T20:30:10+01:00 Download 360a92f
Download 6dd0a7f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 22 2018-12-09T18:21:10+01:00 Download 8be3a71
Download 1789464 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 22 2018-12-08T23:44:51+01:00 Download 8daa4d8
Download 68ed615 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 22 2018-12-08T22:07:45+01:00 Download 8e13c08
Download c40fb90 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 22 2018-12-08T09:07:27+01:00 Download 2543ffc
Download 403a57c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 22 2018-12-08T04:59:28+01:00 Download 5fc25ee
Download e88ccaa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 22 2018-12-08T04:12:50+01:00 Download 0b9bd27
Download 601646e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 22 2018-12-07T18:48:24+01:00 Download a51daf1
Download eaa9d14 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 22 2018-12-07T17:45:16+01:00 Download 28f66ee
Download 1e241cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 22 2018-12-07T01:10:58+01:00 Download 97ee15f
Download 664ba45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 22 2018-12-06T10:11:24+01:00 Download 7f4ebd9
Download 7b635e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 22 2018-12-06T09:48:57+01:00 Download 27ee516
Download c2ab5a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 22 2018-12-06T09:12:07+01:00 Download b5c68d7
Download 27ee516 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 22 2018-12-06T02:02:27+01:00
Download 31431c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-10T20:36:32+01:00 Download 492fb4a
Download e60d2d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:15:39+01:00 Download e65918b
Download b82ea2a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T08:17 CET (sv-comp)
Download 534a831 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T07:53 CET (sv-comp)

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

Trying to find witnesses for program (5c29a2f2e6fd473ca90321383d237316a972788e34fdd534748a8440dc3d2534, sv-benchmarks/c/recursive-simple/sum_15x0_false-unreach-call_true-termination.c).

Found 20 witnesses for program sv-benchmarks/c/recursive-simple/sum_15x0_false-unreach-call_true-termination.c, 5c29a2f2e6fd473ca90321383d237316a972788e34fdd534748a8440dc3d2534
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/5c29a2f2e6fd473ca90321383d237316a972788e34fdd534748a8440dc3d2534.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 71d9625 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 3 2017-12-01T22:14 CET (sv-comp)
Download 7a2279a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 13 Sat Dec 2 22:39:35 2017
Download 1497f43 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VIAP 17 2017-12-03T03:57 CET (sv-comp)
Download 1d3e31f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 18 2017-12-02T21:36Z
Download 1e476db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T16:11 CET (sv-comp)
Download 394474e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 4 2017-12-01T20:01 CET (sv-comp)
Download de76148 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 18 2017-12-02T08:39Z
Download 1b45b21 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T23:37:11.062910
Download df5396f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T16:43:58.889164
Download f2e3498 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 10 2017-12-01T20:49 CET (sv-comp)
Download ab59b5f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 10 2017-11-30T17:05 CET (sv-comp)
Download 66af2d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 21 2017-12-01T00:34:29+01:00
Download a53a725 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 9 2017-11-30T20:28:55+01:00
Download 959abfb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 5 2017-11-30T12:05:37+01:00
Download bbde811 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 6 2017-12-02T03:54:46+01:00
Download dfb46cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 14 2017-11-30T15:09 CET (sv-comp)
Download 68334c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 18 2017-12-02T19:58Z
Download 424be15 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T02:09:43.805707
Download 2404071 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T09:08:29.438195
Download 1e2f0c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 13 2017-12-01T13:01 CET (sv-comp)

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

Trying to find witnesses for program (5c29a2f2e6fd473ca90321383d237316a972788e34fdd534748a8440dc3d2534, sv-benchmarks/c/recursive-simple/sum_15x0_false-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/sum_15x0_false-unreach-call_true-termination.c, 5c29a2f2e6fd473ca90321383d237316a972788e34fdd534748a8440dc3d2534
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/5c29a2f2e6fd473ca90321383d237316a972788e34fdd534748a8440dc3d2534.json

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