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_true-unreach-call_true-termination.c
programSHA 4360477418023f9df3257204df098df6ad744e1c266a72b47fd414741c868928
witnessName results-verified/veriabs.2018-12-10_1650.logfiles/sv-comp19_prop-reachsafety.sum_15x0_true-unreach-call_true-termination.c.files/witness.graphml
witnessSHA 46cbc814e19c41a8a18620c8d02814c89e425f9510605868764dd443c2284fb9

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-10T16:16Z
producer Automizer
programfile /home/benchexec/ar_abs_temp/sum_15x0_true_unreach_call_true_termination_c.c
programhash 7f140b11074e684b22c263036fee9fde5b4c087a
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/46cbc814e19c41a8a18620c8d02814c89e425f9510605868764dd443c2284fb9.graphml
witness-sha256 46cbc814e19c41a8a18620c8d02814c89e425f9510605868764dd443c2284fb9
witness-size 6057
witness-type correctness_witness

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

Trying to find witnesses for program (4360477418023f9df3257204df098df6ad744e1c266a72b47fd414741c868928, sv-benchmarks/c/recursive-simple/sum_15x0_true-unreach-call_true-termination.c).

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

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

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

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

Found 15 witnesses for program sv-benchmarks/c/recursive-simple/sum_15x0_true-unreach-call_true-termination.c, 4360477418023f9df3257204df098df6ad744e1c266a72b47fd414741c868928
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/4360477418023f9df3257204df098df6ad744e1c266a72b47fd414741c868928.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 15e97d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-03T22:11 CET (comp)
Download 63c8da0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:13:25+01:00 Download 3418693
Download 1c7eb71 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:13:06+01:00 Download 10a64a1
Download 2e5abe2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:02:37+01:00 Download 6ea4db3
Download 7bf1ea4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-08T00:49:02+01:00 Download d78f34c
Download d0b7cab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-07T23:38:43+01:00 Download c2386a2
Download 6ffe252 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-07T19:45:46+01:00 Download dd9c7ef
Download a3701cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-06T01:50:24+01:00 Download b274833
Download 5b2a7a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-05T19:13:03+01:00 Download f75bca6
Download 65f929f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-04T02:08:02+01:00 Download 15e97d1
Download 7927b6b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-11-30T19:51:18+01:00 Download 6d31acc
Download a67b456 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-11-30T17:22:07+01:00 Download 67ea1d7
Download 67ea1d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 5 2019-11-30T02:19:37+01:00
Download 10a64a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 5 2019-12-01T00:50:55+01:00
Download b34c6eb Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T22:53 CET (comp)

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

Trying to find witnesses for program (4360477418023f9df3257204df098df6ad744e1c266a72b47fd414741c868928, sv-benchmarks/c/recursive-simple/sum_15x0_true-unreach-call_true-termination.c).

Found 22 witnesses for program sv-benchmarks/c/recursive-simple/sum_15x0_true-unreach-call_true-termination.c, 4360477418023f9df3257204df098df6ad744e1c266a72b47fd414741c868928
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/4360477418023f9df3257204df098df6ad744e1c266a72b47fd414741c868928.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download eb55ac2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-07T21:54 CET (sv-comp)
Download 899e13b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T09:09:51
Download 5f44fa1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T07:53 CET (sv-comp)
Download 7a7c241 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-07T10:08:52+01:00
Download 90790aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-10T19:56:31+01:00 Download 46cbc81
Download 223b572 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-10T10:31:21+01:00 Download 095e513
Download aba49d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T21:06:30+01:00 Download 2514e90
Download 13c4436 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:18:14+01:00 Download 0a41781
Download 17b1a39 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:01:18+01:00 Download 394e785
Download 422fcdb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T23:14:37+01:00 Download eb55ac2
Download 2f15eaf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T21:36:09+01:00 Download 899e13b
Download b1e2d94 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T06:31:06+01:00 Download 7a7c241
Download 6afc3c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T03:09:44+01:00 Download d6b5627
Download 5f2e582 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T02:38:31+01:00 Download 095e513
Download 15ba174 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-07T17:43:35+01:00 Download d7adc63
Download 2da4803 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-07T16:39:03+01:00 Download 5f44fa1
Download 6ebebe3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:28:50+01:00 Download 878e199
Download fe9b9c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T08:45:26+01:00 Download 4f8cd41
Download 74e6ad7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T08:24:52+01:00 Download a5dcb48
Download 4f8cd41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T07:50:47+01:00
Download 0e105bc Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T09:51 CET (sv-comp)
Download a0c2273 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T05:14 CET (sv-comp)

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

Trying to find witnesses for program (4360477418023f9df3257204df098df6ad744e1c266a72b47fd414741c868928, sv-benchmarks/c/recursive-simple/sum_15x0_true-unreach-call_true-termination.c).

Found 31 witnesses for program sv-benchmarks/c/recursive-simple/sum_15x0_true-unreach-call_true-termination.c, 4360477418023f9df3257204df098df6ad744e1c266a72b47fd414741c868928
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/4360477418023f9df3257204df098df6ad744e1c266a72b47fd414741c868928.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 25c5866 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 9 2017-11-30T17:45:09+01:00
Download aa45cfe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 5 2017-11-30T13:50:51+01:00
Download f66f794 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 6 2017-12-02T02:08:16+01:00
Download d7adc63 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T22:57 CET (sv-comp)
Download 1b79adf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness VIAP 16 2017-12-03T04:05 CET (sv-comp)
Download 07ff445 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 6 2017-12-02T20:40Z
Download aa1d33e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T02:44 CET (sv-comp)
Download 7b242e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 4 2017-12-01T21:13 CET (sv-comp)
Download 43bcc45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T00:03:30.246530
Download b9dfb86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T13:29:42.936935
Download ee1cfc1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T21:55:55.814996
Download c0bc00e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T07:49:53.680305
Download d14fd62 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 5 2017-12-01T18:43 CET (sv-comp)
Download b2d6ae2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.12-svcomp17 4 2017-11-02T13:16:17+05:30
Download d862d20 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 6 2017-11-30T21:41:13+01:00
Download 861f63e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T06:51:40+01:00 f353219
Download 35a0fac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T04:22:25+01:00 6c5d8a3
Download 13d925a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T04:09:38+01:00 0875aac
Download 8c8b620 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T00:10:27+01:00 f1fa808
Download 255dfff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T20:11:28+01:00 182f764
Download 3e259e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T08:46:11+01:00 65b93d0
Download a458744 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T00:11:15+01:00 56c5289
Download 26f99ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T22:27:54+01:00 7a64c64
Download a0f28e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T22:08:44+01:00 200e847
Download 18162b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T08:13:49+01:00 3f72f06
Download a9e5807 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T06:16:30+01:00 b967d86
Download b6090eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T05:13:34+01:00 9aa04c9
Download 589da8c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-11-30T17:01:06+01:00
Download 804b93d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 13 2017-12-01T01:57 CET (sv-comp)
Download 9993de3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 6 2017-12-02T05:24Z
Download 1ae17bf Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 13 2017-12-01T19:19 CET (sv-comp)

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

Trying to find witnesses for program (4360477418023f9df3257204df098df6ad744e1c266a72b47fd414741c868928, sv-benchmarks/c/recursive-simple/sum_15x0_true-unreach-call_true-termination.c).

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

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