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/id_i15_o15_false-unreach-call_true-termination.c
programSHA 0c91304606bed46cc1c2477c2455c3c7e73c03bf5dec4bb2f024ae3cb346c827
witnessName results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.id_i15_o15_false-unreach-call_true-termination.c.files/witness.graphml
witnessSHA 3c2b0dc99b298f71130f3dc569994214ca30dce69e8719f7437f234382f7a846

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-11-30T15:23:12+01:00
producer CPAchecker 1.6.1-svn 26773
program-sha256 0c91304606bed46cc1c2477c2455c3c7e73c03bf5dec4bb2f024ae3cb346c827
programfile ../../sv-benchmarks/c/recursive-simple/id_i15_o15_false-unreach-call_true-termination.c
programhash ad4e6ad99a266ddeead98987e8e44db723af5bc7
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/3c2b0dc99b298f71130f3dc569994214ca30dce69e8719f7437f234382f7a846.graphml
witness-sha256 3c2b0dc99b298f71130f3dc569994214ca30dce69e8719f7437f234382f7a846
witness-size 20976
witness-type violation_witness

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

Trying to find witnesses for program (0c91304606bed46cc1c2477c2455c3c7e73c03bf5dec4bb2f024ae3cb346c827, sv-benchmarks/c/recursive-simple/id_i15_o15_false-unreach-call_true-termination.c).

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download fcf0466 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 01:16:05
Download 616fef6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 11 2019-12-03T23:12 CET (comp)
Download e451d9e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 21 2019-12-11T21:51:19+01:00 Download 9fe3893
Download 0602c91 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 21 2019-12-11T21:40:21+01:00 Download c253f52
Download 081e4a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 21 2019-12-11T21:09:41+01:00 Download fcf0466
Download 64803ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 21 2019-12-11T20:54:22+01:00 Download 0d9e4c1
Download 77551b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 21 2019-12-11T20:44:51+01:00 Download 55b208a
Download 6e45e45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 21 2019-12-08T00:26:02+01:00 Download 221a4a8
Download febcd83 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 21 2019-12-07T21:15:29+01:00 Download b1a00b8
Download 0ac16b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 21 2019-12-06T02:40:14+01:00 Download 104314f
Download 173256f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 21 2019-12-04T02:58:30+01:00 Download 616fef6
Download 6766870 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 21 2019-12-03T08:56:47+01:00 Download 505e9fe
Download 6bc1875 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 21 2019-12-03T08:00:34+01:00 Download 89500a9
Download 89500a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 21 2019-11-30T01:58:47+01:00
Download c253f52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 21 2019-11-30T21:19:35+01:00
Download 61cb71e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-08T01:51:37+01:00 Download 1468e7c
Download 3b3cb3e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-05T20:20:23+01:00 Download c518285
Download 5a165b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T00:07 CET (comp)

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

Trying to find witnesses for program (0c91304606bed46cc1c2477c2455c3c7e73c03bf5dec4bb2f024ae3cb346c827, sv-benchmarks/c/recursive-simple/id_i15_o15_false-unreach-call_true-termination.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 65f1e87 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T13:05 CET (sv-comp)
Download 776d9a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T01:34:11
Download a5472f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 12 2018-12-06T22:35 CET (sv-comp)
Download 6b48ac3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 21 2018-12-08T00:29:52+01:00
Download 3bba2db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 21 2018-12-10T10:48:45+01:00 Download c4ddcff
Download 7a03be8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 21 2018-12-09T21:23:34+01:00 Download d8e1d13
Download 159c41c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 21 2018-12-09T20:53:05+01:00 Download a04c5b1
Download 9175e26 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 21 2018-12-09T20:37:42+01:00 Download 72846ac
Download db03522 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 21 2018-12-09T20:31:33+01:00 Download 3c5bee9
Download 566f45d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 21 2018-12-09T18:20:53+01:00 Download 7a29599
Download 9a07c00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 21 2018-12-08T23:43:47+01:00 Download 65f1e87
Download c315544 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 21 2018-12-08T22:07:31+01:00 Download 776d9a6
Download 774e827 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 21 2018-12-08T08:20:22+01:00 Download 6b48ac3
Download 723ac9a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 21 2018-12-08T05:01:01+01:00 Download d1209a3
Download 74d407b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 21 2018-12-08T03:42:22+01:00 Download c4ddcff
Download 73d66e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 21 2018-12-07T18:26:27+01:00 Download ea9686b
Download dd83961 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 22 2018-12-07T17:09:50+01:00 Download a5472f8
Download 6070f3d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 21 2018-12-07T01:06:21+01:00 Download 555fae7
Download 1a88e2d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 21 2018-12-06T10:11:09+01:00 Download 578b98f
Download 6088c93 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 21 2018-12-06T09:47:55+01:00 Download 1ac8107
Download 3be5278 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 22 2018-12-06T09:06:31+01:00 Download e93e078
Download 1ac8107 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 21 2018-12-05T18:57:57+01:00
Download a6bd999 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-10T20:35:01+01:00 Download 4c713ea
Download 332dbbd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:17:16+01:00 Download 688b130
Download 22393a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T14:02 CET (sv-comp)
Download 9fdfabb Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T02:20 CET (sv-comp)

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

Trying to find witnesses for program (0c91304606bed46cc1c2477c2455c3c7e73c03bf5dec4bb2f024ae3cb346c827, sv-benchmarks/c/recursive-simple/id_i15_o15_false-unreach-call_true-termination.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6002bcb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 3 2017-12-01T23:14 CET (sv-comp)
Download 2e47069 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 13 Sat Dec 2 23:25:32 2017
Download d8e1d13 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VIAP 16 2017-12-03T03:59 CET (sv-comp)
Download 16f623b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 17 2017-12-03T02:52Z
Download 07613d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T02:40 CET (sv-comp)
Download 15a1740 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 3 2017-12-01T20:57 CET (sv-comp)
Download 07f24b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 17 2017-12-02T10:13Z
Download 17405f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T21:12:29.142320
Download 0ff6ca2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T18:48:58.185056
Download e6fdd81 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 7 2017-12-01T21:37 CET (sv-comp)
Download f0cc16c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 7 2017-12-01T01:31 CET (sv-comp)
Download 3c2b0dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 21 2017-11-30T15:23:12+01:00
Download 674ee6b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 9 2017-11-30T12:34:30+01:00
Download 9cc9594 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 5 2017-11-30T22:24:18+01:00
Download 13c6918 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 6 2017-12-01T20:09:47+01:00
Download 180bc6c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 14 2017-11-30T13:08 CET (sv-comp)
Download ab7f94b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 17 2017-12-02T10:18Z
Download ff02e9a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T22:57:10.208282
Download 7e256bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T13:10:54.929509
Download 4e2864c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 13 2017-12-01T15:01 CET (sv-comp)

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

Trying to find witnesses for program (0c91304606bed46cc1c2477c2455c3c7e73c03bf5dec4bb2f024ae3cb346c827, sv-benchmarks/c/recursive-simple/id_i15_o15_false-unreach-call_true-termination.c).

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

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