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_o10_false-unreach-call_true-termination_true-no-overflow.c
programSHA 6c018b94e33ff7d445012abcec0add246fec195e247b0a070a2536154de548b7
witnessName results-verified/utaipan.2017-12-03_0843.logfiles/sv-comp18.id_o10_false-unreach-call_true-termination_true-no-overflow.c.files/witness.graphml
witnessSHA 46fca53070f0d1a34632a1cc6159f4c36e2d34b140e2603b89c5203552aec07e

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-03T07:44Z
producer Taipan
program-sha256 6c018b94e33ff7d445012abcec0add246fec195e247b0a070a2536154de548b7
programfile /tmp/vcloud-vcloud-master/worker/working_dir_4173fcd5-e537-424a-b53c-b367bf1a6407/sv-benchmarks/c/recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c
programhash 0c292d0c9d9c055df9398b3303a92d6621b60758
sourcecodelang C
specification CHECK( init(main()), LTL(G ! overflow) )
witness-file witnessFileByHash/46fca53070f0d1a34632a1cc6159f4c36e2d34b140e2603b89c5203552aec07e.graphml
witness-sha256 46fca53070f0d1a34632a1cc6159f4c36e2d34b140e2603b89c5203552aec07e
witness-size 5709
witness-type correctness_witness

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

Trying to find witnesses for program (6c018b94e33ff7d445012abcec0add246fec195e247b0a070a2536154de548b7, sv-benchmarks/c/recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c, 6c018b94e33ff7d445012abcec0add246fec195e247b0a070a2536154de548b7
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/6c018b94e33ff7d445012abcec0add246fec195e247b0a070a2536154de548b7.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 (6c018b94e33ff7d445012abcec0add246fec195e247b0a070a2536154de548b7, sv-benchmarks/c/recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c, 6c018b94e33ff7d445012abcec0add246fec195e247b0a070a2536154de548b7
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/6c018b94e33ff7d445012abcec0add246fec195e247b0a070a2536154de548b7.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 (6c018b94e33ff7d445012abcec0add246fec195e247b0a070a2536154de548b7, sv-benchmarks/c/recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c, 6c018b94e33ff7d445012abcec0add246fec195e247b0a070a2536154de548b7
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/6c018b94e33ff7d445012abcec0add246fec195e247b0a070a2536154de548b7.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 (6c018b94e33ff7d445012abcec0add246fec195e247b0a070a2536154de548b7, sv-benchmarks/c/recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c, 6c018b94e33ff7d445012abcec0add246fec195e247b0a070a2536154de548b7
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/6c018b94e33ff7d445012abcec0add246fec195e247b0a070a2536154de548b7.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 (6c018b94e33ff7d445012abcec0add246fec195e247b0a070a2536154de548b7, sv-benchmarks/c/recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c).

Found 17 witnesses for program sv-benchmarks/c/recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c, 6c018b94e33ff7d445012abcec0add246fec195e247b0a070a2536154de548b7
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/6c018b94e33ff7d445012abcec0add246fec195e247b0a070a2536154de548b7.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 12f1a35 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 5 2019-11-30T14:05:40+01:00
Download d7e9251 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 5 2019-12-01T07:56:56+01:00
Download ac2fa7f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 23:59:29
Download aecae15 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 16 2019-12-11T22:00:45+01:00 Download d6617e0
Download d802dcb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 16 2019-12-11T21:44:42+01:00 Download 5941fe0
Download 37527ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 16 2019-12-11T21:09:18+01:00 Download ac2fa7f
Download 037a1e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 16 2019-12-11T20:44:33+01:00 Download 62e8db7
Download ded5bab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 16 2019-12-08T00:26:03+01:00 Download 614f92e
Download 2669855 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 16 2019-12-07T21:17:27+01:00 Download c159cb4
Download 3e929cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 16 2019-12-06T02:41:02+01:00 Download c31f2f0
Download 82585de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 16 2019-12-05T20:20:34+01:00 Download 05be625
Download c03fe0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 16 2019-12-03T08:57:35+01:00 Download 33bc6d5
Download a4926fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 16 2019-12-03T08:08:16+01:00 Download e2fe07f
Download e2fe07f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 16 2019-11-30T08:06:46+01:00
Download 5941fe0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 16 2019-11-30T23:55:24+01:00
Download 87de51f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:55:21+01:00 Download b188952
Download b77641c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-08T01:52:24+01:00 Download 3e6a3e5

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

Trying to find witnesses for program (6c018b94e33ff7d445012abcec0add246fec195e247b0a070a2536154de548b7, sv-benchmarks/c/recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c).

Found 28 witnesses for program sv-benchmarks/c/recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c, 6c018b94e33ff7d445012abcec0add246fec195e247b0a070a2536154de548b7
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/6c018b94e33ff7d445012abcec0add246fec195e247b0a070a2536154de548b7.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 47b3d4b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 1 2018-12-08T10:45 CET (sv-comp)
Download 5ffca8f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness SMACK 1.9.3 3 2018-12-08T01:06:10
Download 9c90fb8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-08T03:34:25+01:00
Download 7a8875b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-05T18:32:28+01:00
Download 38f63bb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-07T23:33 CET (sv-comp)
Download 4890904 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T06:12:48
Download d72ff8d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 10 2018-12-06T20:25 CET (sv-comp)
Download 654e077 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 16 2018-12-08T01:05:37+01:00
Download 2b19669 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-09T21:23:30+01:00 Download f594154
Download 510192d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-09T20:53:09+01:00 Download 11a7996
Download bf63eb0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-09T20:38:47+01:00 Download 8069b2b
Download 9abf901 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-09T20:22:56+01:00 Download 20f5fad
Download 45f0696 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-09T18:21:05+01:00 Download 2f81920
Download f0fe31c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-08T23:44:04+01:00 Download 38f63bb
Download 2032dc6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-08T22:07:43+01:00 Download 4890904
Download 3437785 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-08T08:52:42+01:00 Download 654e077
Download 7235297 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-08T04:54:59+01:00 Download 1ff1722
Download 3f2f236 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-08T04:35:28+01:00 Download a4b46f0
Download ef869dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-07T18:31:43+01:00 Download 851fd2b
Download 771b330 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-07T17:45:24+01:00 Download d72ff8d
Download aad156c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-06T10:18:47+01:00 Download 2ba722c
Download 0063485 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-06T09:48:00+01:00 Download 2f0464c
Download 9a9ae4e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-06T09:18:08+01:00 Download 876b01d
Download ba7ac44 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-06T09:09:17+01:00 Download d7f21ea
Download 2f0464c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-05T22:08:59+01:00
Download 2320d7a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-10T20:35:06+01:00 Download 785683d
Download a65a619 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-07T01:09:47+01:00 Download cc4699c
Download 5591e84 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T13:49 CET (sv-comp)

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

Trying to find witnesses for program (6c018b94e33ff7d445012abcec0add246fec195e247b0a070a2536154de548b7, sv-benchmarks/c/recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c).

Found 23 witnesses for program sv-benchmarks/c/recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c, 6c018b94e33ff7d445012abcec0add246fec195e247b0a070a2536154de548b7
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/6c018b94e33ff7d445012abcec0add246fec195e247b0a070a2536154de548b7.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 46fca53 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 6 2017-12-03T07:44Z
Download 399a689 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 1 2017-12-03T04:42 CET (sv-comp)
Download f445704 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 6 2017-12-03T10:25Z
Download d7f8ca2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 3.1 5 2017-12-01T14:05 CET (sv-comp)
Download 54cadb6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T11:39:19+01:00
Download 174b998 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 6 2017-12-03T10:36Z
Download 356ee6e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 3 2017-12-01T22:27 CET (sv-comp)
Download 8718f83 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 11 Sat Dec 2 18:41:17 2017
Download 6068bc8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VIAP 4 2017-12-03T03:50 CET (sv-comp)
Download d0936d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 14 2017-12-02T19:49Z
Download af6e860 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-01T22:42 CET (sv-comp)
Download 2114fd0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 2 2017-12-01T19:59 CET (sv-comp)
Download c8fc163 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 14 2017-12-02T03:43Z
Download 1cbacc6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T18:49:54.508414
Download ca76ca5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T09:08:06.261060
Download 628b165 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 6 2017-12-01T17:45 CET (sv-comp)
Download 370d816 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 6 2017-12-01T06:41 CET (sv-comp)
Download 8c4b7b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 16 2017-11-30T11:48:10+01:00
Download 85924ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 10 2017-11-30T17:04:19+01:00
Download e73437d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 5 2017-11-30T19:58:01+01:00
Download b50b991 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 6 2017-12-01T23:09:42+01:00
Download 14f564b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 11 2017-11-30T14:40 CET (sv-comp)
Download 836521a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 14 2017-12-02T10:40Z

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

Trying to find witnesses for program (6c018b94e33ff7d445012abcec0add246fec195e247b0a070a2536154de548b7, sv-benchmarks/c/recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c, 6c018b94e33ff7d445012abcec0add246fec195e247b0a070a2536154de548b7
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/6c018b94e33ff7d445012abcec0add246fec195e247b0a070a2536154de548b7.json

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